inductive beta_red : Trm → Trm → Prop

• br_beta (t1 t2 : Trm) (T : Typ) : (λ T,t1).lc → t2.lc → beta_red ((λ T,t1) @ t2) (t1.open₀ t2)
• br_app1 (t1 t1' t2 : Trm) : t2.lc → beta_red t1 t1' → beta_red (t1 @ t2) (t1' @ t2)
• br_app2 (t1 t2 t2' : Trm) : t1.lc → beta_red t2 t2' → beta_red (t1 @ t2) (t1 @ t2')
• br_abs (t1 t1' : Trm) (T : Typ) (L : Finset ℕ) : (∀ x ∉ L, beta_red (t1.open₀ ($x)) (t1'.open₀ ($x))) → beta_red (λ T,t1) (λ T,t1')

theorem beta_red_regular (t1 t2 : Trm) : beta_red t1 t2 → t1.lc ∧ t2.lc

theorem beta_rename (t1 t2 : Trm) (x y : ℕ) : beta_red t1 t2 → beta_red ([x // $y] t1) ([x // $y] t2)

theorem beta_abs_intro (t1 t2 : Trm) (T : Typ) (x : ℕ) : beta_red (t1.open₀ ($x)) (t2.open₀ ($x)) → x ∉ t1.fv → x ∉ t2.fv → beta_red (λ T,t1) (λ T,t2)

theorem beta_red_subst_out (t1 t2 : Trm) (x : ℕ) (u : Trm) : beta_red t1 t2 ∧ u.lc → beta_red ([x // u] t1) ([x // u] t2)

inductive para : Trm → Trm → Prop

• para_var (x : ℕ) : para ($x) ($x)
• para_red (t1 t1' t2 t2' : Trm) (T : Typ) (L : Finset ℕ) : (∀ x ∉ L, para (t1.open₀ ($x)) (t1'.open₀ ($x))) → para t2 t2' → para ((λ T,t1) @ t2) (t1'.open₀ t2')
• para_app (t1 t1' t2 t2' : Trm) : para t1 t1' → para t2 t2' → para (t1 @ t2) (t1' @ t2')
• para_abs (t1 t1' : Trm) (T : Typ) (L : Finset ℕ) : (∀ x ∉ L, para (t1.open₀ ($x)) (t1'.open₀ ($x))) → para (λ T,t1) (λ T,t1')

theorem para_regular (t1 t2 : Trm) : para t1 t2 → t1.lc ∧ t2.lc

theorem lc_para_refl (t : Trm) : t.lc → para t t

theorem para_subst_all (t1 t2 s1 s2 : Trm) : para t1 t2 → para s1 s2 → ∀ (x : ℕ), para ([x // s1] t1) ([x // s2] t2)

theorem para_open_out (t t' u u' : Trm) (L : Finset ℕ) : (∀ x ∉ L, para (t.open₀ ($x)) (u.open₀ ($x))) → para t' u' → para (t.open₀ t') (u.open₀ u')

theorem opening_closing_para (t u : Trm) (x y z : ℕ) : para t u → y ∉ t.fv ∪ u.fv ∪ {x} → para ( {z ~> $y} { z <~ x } t) ( {z ~> $y} { z <~ x } u)

theorem open_close_para (t u : Trm) (x y : ℕ) : para t u → y ∉ t.fv ∪ u.fv ∪ {x} → para ((t.close₀ x).open₀ ($y)) ((u.close₀ x).open₀ ($y))

theorem para_through (t1 t2 u1 u2 : Trm) (x : ℕ) : x ∉ t1.fv ∧ x ∉ t2.fv → para (t1.open₀ ($x)) (t2.open₀ ($x)) → para u1 u2 → para (t1.open₀ u1) (t2.open₀ u2)

inductive multi_red : Trm → Trm → Prop

• mr_refl (t : Trm) : t.lc → multi_red t t
• mr_head (t1 t2 t3 : Trm) : multi_red t1 t2 → beta_red t2 t3 → multi_red t1 t3

theorem multi_red_trans (t1 t2 t3 : Trm) : multi_red t1 t2 → multi_red t2 t3 → multi_red t1 t3

theorem multi_red_regular (t1 t2 : Trm) : multi_red t1 t2 → t1.lc ∧ t2.lc

theorem beta_to_multi_red (t1 t2 : Trm) : beta_red t1 t2 → multi_red t1 t2

theorem multi_red_abs_intro' (u1 u2 : Trm) (T : Typ) (x : ℕ) : multi_red u1 u2 → ∀ (t1 t2 : Trm), u1 = t1.open₀ ($x) → u2 = t2.open₀ ($x) → x ∉ t1.fv → x ∉ t2.fv → multi_red (λ T,t1) (λ T,t2)

theorem multi_red_abs_intro (t1 t2 : Trm) (T : Typ) (x : ℕ) : multi_red (t1.open₀ ($x)) (t2.open₀ ($x)) → x ∉ t1.fv → x ∉ t2.fv → multi_red (λ T,t1) (λ T,t2)

theorem multi_red_abs (t1 t2 : Trm) (T : Typ) (L : Finset ℕ) : (∀ x ∉ L, multi_red (t1.open₀ ($x)) (t2.open₀ ($x))) → multi_red (λ T,t1) (λ T,t2)

theorem multi_red_app1 (t1 t1' t2 : Trm) : multi_red t1 t1' ∧ t2.lc → multi_red (t1 @ t2) (t1' @ t2)

theorem multi_red_app2 (t1 t2 t2' : Trm) : multi_red t2 t2' ∧ t1.lc → multi_red (t1 @ t2) (t1 @ t2')

theorem multi_red_subst_in (t : Trm) (x : ℕ) (u1 u2 : Trm) : multi_red u1 u2 ∧ t.lc → multi_red ([x // u1] t) ([x // u2] t)

theorem multi_red_subst_all (t1 t2 : Trm) (x : ℕ) (u1 u2 : Trm) : multi_red t1 t2 ∧ multi_red u1 u2 → multi_red ([x // u1] t1) ([x // u2] t2)

theorem multi_red_through (t1 t2 u1 u2 : Trm) (x : ℕ) : x ∉ t1.fv ∧ x ∉ t2.fv → multi_red (t1.open₀ ($x)) (t2.open₀ ($x)) → multi_red u1 u2 → multi_red (t1.open₀ u1) (t2.open₀ u2)

inductive multi_para : Trm → Trm → Prop

• m_para_refl (t : Trm) : t.lc → multi_para t t
• m_para_head (t1 t2 t3 : Trm) : multi_para t1 t2 → para t2 t3 → multi_para t1 t3

theorem multi_para_trans (t1 t2 t3 : Trm) : multi_para t1 t2 → multi_para t2 t3 → multi_para t1 t3

theorem multi_para_regular (t1 t2 : Trm) : multi_para t1 t2 → t1.lc ∧ t2.lc

theorem para_to_multi_para (t1 t2 : Trm) : para t1 t2 → multi_para t1 t2

theorem beta_red_to_para (t t' : Trm) : beta_red t t' → para t t'

theorem multi_red_to_multi_para (t t' : Trm) : multi_red t t' → multi_para t t'

theorem para_to_multi_red (t t' : Trm) : para t t' → multi_red t t'

theorem multi_para_to_multi_red (t t' : Trm) : multi_para t t' → multi_red t t'

theorem multi_red_iff_multi_para (t1 t2 : Trm) : multi_red t1 t2 ↔ multi_para t1 t2