def Trm.opening (k : ℕ) (u : Trm) : Trm → Trm

Equations

• ( {k ~> u} €i) = if k = i then u else €i
• ( {k ~> u} $x_1) = $x_1
• ( {k ~> u} λ T,t) = λ T, {k + 1 ~> u} t
• ( {k ~> u} t1 @ t2) = ( {k ~> u} t1) @ {k ~> u} t2

def Trm.«term{_~>_}_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Trm.open₀ (t u : Trm) : Trm

Equations

• t.open₀ u = {0 ~> u} t

theorem Trm.open_var_fv (t u : Trm) (k : ℕ) : ( {k ~> u} t).fv ⊆ t.fv ∪ u.fv

theorem Trm.opening_lc_lemma (t u v : Trm) (i j : ℕ) : i ≠ j → (( {j ~> u} t) = {i ~> v} {j ~> u} t) → t = {i ~> v} t

def Trm.closing (k x : ℕ) : Trm → Trm

Equations

• ( { k <~ x } €i) = €i
• ( { k <~ x } $x_2) = if x = x_2 then €k else $x_2
• ( { k <~ x } λ T,t) = λ T, { k + 1 <~ x } t
• ( { k <~ x } t1 @ t2) = ( { k <~ x } t1) @ { k <~ x } t2

def Trm.«term{_<~_}_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Trm.close₀ (u : Trm) (x : ℕ) : Trm

Equations

• u.close₀ x = { 0 <~ x } u

theorem Trm.close_var_fv (t : Trm) (x k : ℕ) : ( { k <~ x } t).fv = t.fv \ {x}

inductive Trm.lc : Trm → Prop

• lc_var (x : ℕ) : ($x).lc
• lc_abs (t : Trm) (T : Typ) (L : Finset ℕ) : (∀ x ∉ L, (t.open₀ ($x)).lc) → (λ T,t).lc
• lc_app (t1 t2 : Trm) : t1.lc → t2.lc → (t1 @ t2).lc

def Trm.body (t : Trm) : Prop

Equations

• t.body = ∃ (L : Finset ℕ), ∀ x ∉ L, (t.open₀ ($x)).lc

theorem Trm.lc_abs_iff_body (t : Trm) (T : Typ) : (λ T,t).lc ↔ t.body

theorem Trm.close_open (x : ℕ) (t : Trm) : x ∉ t.fv → ∀ (k : ℕ), ( { k <~ x } {k ~> $x} t) = t

theorem Trm.close_open_var (x : ℕ) (t : Trm) : x ∉ t.fv → (t.open₀ ($x)).close₀ x = t

theorem Trm.open₀_injective (x : ℕ) (t1 t2 : Trm) : x ∉ t1.fv → x ∉ t2.fv → t1.open₀ ($x) = t2.open₀ ($x) → t1 = t2

theorem Trm.open_close_lemma (x y z : ℕ) (t : Trm) : x ≠ y → y ∉ t.fv → ∀ (i j : ℕ), i ≠ j → ( {i ~> $y} {j ~> $z} { j <~ x } t) = {j ~> $z} { j <~ x } {i ~> $y} t

theorem Trm.open_close (x : ℕ) (t : Trm) : t.lc → ∀ (k : ℕ), ( {k ~> $x} { k <~ x } t) = t

theorem Trm.open_close_var (x : ℕ) (t : Trm) : t.lc → (t.close₀ x).open₀ ($x) = t

theorem Trm.closing_injective (x i : ℕ) (t1 t2 : Trm) : t1.lc → t2.lc → (( { i <~ x } t1) = { i <~ x } t2) → t1 = t2

theorem Trm.opening_lc (t u : Trm) : t.lc → ∀ (k : ℕ), t = {k ~> u} t

theorem Trm.open₀_lc (t u : Trm) : t.lc → t = t.open₀ u

theorem Trm.subst_open_rec (t1 t2 u : Trm) (i j : ℕ) : u.lc → ([i // u] {j ~> t2} t1) = {j ~> [i // u] t2} [i // u] t1

theorem Trm.subst_open_var (t u : Trm) : u.lc → ∀ (i j : ℕ), i ≠ j → ([i // u] t).open₀ ($j) = [i // u] t.open₀ ($j)

theorem Trm.subst_intro (t u : Trm) : u.lc → ∀ x ∉ t.fv, t.open₀ u = [x // u] t.open₀ ($x)

theorem Trm.subst_lc (t u : Trm) (x : ℕ) : t.lc → u.lc → ([x // u] t).lc

theorem Trm.open_var_body (x : ℕ) (t : Trm) : t.body → (t.open₀ ($x)).lc

theorem Trm.open_var_lc {T : Typ} (x : ℕ) (t : Trm) : (λ T,t).lc → (t.open₀ ($x)).lc

theorem Trm.open_body (t u : Trm) : t.body → u.lc → (t.open₀ u).lc

theorem Trm.open_lc {T : Typ} (t u : Trm) : (λ T,t).lc → u.lc → (t.open₀ u).lc

theorem Trm.open_close_subst (t : Trm) (x y : ℕ) : t.lc → ∀ (k : ℕ), ( {k ~> $y} { k <~ x } t) = [x // $y] t