theorem LambdaCalculus.LocallyNameless.Untyped.Term.open_lc_aux {Var : Type u} (e : Term Var) (j : ℕ) (v : Term Var) (i : ℕ) (u : Term Var) (neq : i ≠ j) (eq : openRec j v e = openRec i u (openRec j v e)) : e = openRec i u e

An opening appearing in both sides of an equality of terms can be removed.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.swap_open_fvars {Var : Type u} (k n : ℕ) (x y : Var) (m : Term Var) (neq : k ≠ n) : openRec k (fvar x) (openRec n (fvar y) m) = openRec n (fvar y) (openRec k (fvar x) m)

Opening is associative for nonclashing free variables.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.subst_fresh {Var : Type u} [DecidableEq Var] (x : Var) (t sub : Term Var) (nmem : x ∉ t.fv) : t[x:=sub] = t

Substitution of a free variable not present in a term leaves it unchanged.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.open_close {Var : Type u} [DecidableEq Var] (x : Var) (t : Term Var) (k : ℕ) (nmem : x ∉ t.fv) : t = closeRec k x (openRec k (fvar x) t)

theorem LambdaCalculus.LocallyNameless.Untyped.Term.open_injective {Var : Type u} [DecidableEq Var] (x : Var) (M M' : Term Var) (free_M : x ∉ M.fv) (free_M' : x ∉ M'.fv) (eq : M.open' (fvar x) = M'.open' (fvar x)) : M = M'

Opening is injective.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.swap_open_fvar_close {Var : Type u} [DecidableEq Var] (k n : ℕ) (x y : Var) (m : Term Var) (neq₁ : k ≠ n) (neq₂ : x ≠ y) : closeRec k x (openRec n (fvar y) m) = openRec n (fvar y) (closeRec k x m)

Opening and closing are associative for nonclashing free variables.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.close_preserve_not_fvar {Var : Type u} [DecidableEq Var] {k : ℕ} {x y : Var} (m : Term Var) (nmem : x ∉ m.fv) : x ∉ (closeRec k y m).fv

Closing preserves free variables.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.open_fresh_preserve_not_fvar {Var : Type u} [DecidableEq Var] {k : ℕ} {x y : Var} (m : Term Var) (nmem : x ∉ m.fv) (neq : x ≠ y) : x ∉ (openRec k (fvar y) m).fv

Opening to a fresh free variable preserves free variables.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.subst_preserve_not_fvar {Var : Type u} [DecidableEq Var] {x y : Var} (m n : Term Var) (nmem : x ∉ m.fv ∪ n.fv) : x ∉ m[y:=n].fv

Substitution preserves free variables.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.close_var_not_fvar_rec {Var : Type u} [DecidableEq Var] (x : Var) (k : ℕ) (t : Term Var) : x ∉ (closeRec k x t).fv

Closing removes a free variable.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.close_var_not_fvar {Var : Type u} [DecidableEq Var] (x : Var) (t : Term Var) : x ∉ (t.close x).fv

Specializes close_var_not_fvar_rec to first closing.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.open_lc {Var : Type u} [HasFresh Var] (k : ℕ) (t e : Term Var) (e_lc : e.LC) : e = openRec k t e

A locally closed term is unchanged by opening.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.subst_openRec {Var : Type u} [DecidableEq Var] [HasFresh Var] (x : Var) (t : Term Var) (k : ℕ) (u e : Term Var) (lc : t.LC) : (openRec k u e)[x:=t] = openRec k (u[x:=t]) (e[x:=t])

Substitution of a locally closed term distributes with opening.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.subst_open {Var : Type u} [DecidableEq Var] [HasFresh Var] (x : Var) (t u e : Term Var) (lc : t.LC) : (e.open' u)[x:=t] = e[x:=t].open' (u[x:=t])

Specialize subst_openRec to the first opening.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.subst_open_var {Var : Type u} [DecidableEq Var] [HasFresh Var] (x y : Var) (u e : Term Var) (neq : y ≠ x) (u_lc : u.LC) : (e.open' (fvar x))[y:=u] = e[y:=u].open' (fvar x)

Specialize subst_open to the free variables.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.subst_lc {Var : Type u} [DecidableEq Var] [HasFresh Var] {x : Var} {e u : Term Var} (e_lc : e.LC) (u_lc : u.LC) : e[x:=u].LC

Substitution of locally closed terms is locally closed.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.subst_intro {Var : Type u} [DecidableEq Var] [HasFresh Var] (x : Var) (t e : Term Var) (mem : x ∉ e.fv) (t_lc : t.LC) : e.open' t = (e.open' (fvar x))[x:=t]

Opening to a term t is equivalent to opening to a free variable and substituting for t.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.beta_lc {Var : Type u} [DecidableEq Var] [HasFresh Var] {M N : Term Var} (m_lc : M.abs.LC) (n_lc : N.LC) : (M.open' N).LC

Opening of locally closed terms is locally closed.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.open_close_to_subst {Var : Type u} [DecidableEq Var] [HasFresh Var] (m : Term Var) (x y : Var) (k : ℕ) (m_lc : m.LC) : openRec k (fvar y) (closeRec k x m) = m[x:=fvar y]

Opening then closing is equivalent to substitution.

theorem LambdaCalculus.LocallyNameless.Untyped.Term.close_open {Var : Type u} [DecidableEq Var] [HasFresh Var] (x : Var) (t : Term Var) (k : ℕ) (t_lc : t.LC) : openRec k (fvar x) (closeRec k x t) = t

Closing and opening are inverses.