From 9412068af5acd547e32f1951f10462ce92adb268 Mon Sep 17 00:00:00 2001
From: Haoxuan Yin <haoxn.yin@gmail.com>
Date: Tue, 10 Mar 2026 15:43:15 +0800
Subject: [PATCH 1/9] rewrite definition of alpha equivalence and substitution
 for named lambda calculus

---
 .../LambdaCalculus/Named/Untyped/Basic.lean   | 91 +++++++------------
 1 file changed, 31 insertions(+), 60 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
index c6adcca35..a011f2270 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fabrizio Montesi
+Authors: Fabrizio Montesi, Haoxuan Yin
 -/
 
 module
@@ -19,6 +19,7 @@ The untyped λ-calculus.
 ## References
 
 * [H. Barendregt, *Introduction to Lambda Calculus*][Barendregt1984]
+* Definition of α-equivalence [A. Pitts, *Nominal Techniques*][Pitts2015]
 
 -/
 
@@ -50,27 +51,17 @@ def Term.bv [DecidableEq Var] : Term Var → Finset Var
   | app m n => m.bv ∪ n.bv
 
 /-- Variable names (free and bound) in a term. -/
-def Term.vars [DecidableEq Var] (m : Term Var) : Finset Var :=
-  m.fv ∪ m.bv
-
-/-- Capture-avoiding substitution, as an inference system. -/
-inductive Term.Subst [DecidableEq Var] : Term Var → Var → Term Var → Term Var → Prop where
-  | varHit : (var x).Subst x r r
-  | varMiss : x ≠ y → (var y).Subst x r (var y)
-  | absShadow : (abs x m).Subst x r (abs x m)
-  | absIn : x ≠ y → y ∉ r.fv → m.Subst x r m' → (abs y m).Subst x r (abs y m')
-  | app : m.Subst x r m' → n.Subst x r n' → (app m n).Subst x r (app m' n')
+def Term.vars [DecidableEq Var] : Term Var → Finset Var
+  | var x => {x}
+  | abs x m => m.vars ∪ {x}
+  | app m n => m.vars ∪ n.vars
 
-/-- Renaming, or variable substitution. `m.rename x y` renames `x` into `y` in `m`. -/
+/-- Variable renaming, applying to both free and bound variables.
+    `m.rename x y` changes all occurrences of `x` into `y` in `m`. -/
 def Term.rename [DecidableEq Var] (m : Term Var) (x y : Var) : Term Var :=
   match m with
   | var z => if z = x then (var y) else (var z)
-  | abs z m' =>
-    if z = x then
-      -- Shadowing
-      abs z m'
-    else
-      abs z (m'.rename x y)
+  | abs z m' => abs (if z = x then y else z) (m'.rename x y)
   | app n1 n2 => app (n1.rename x y) (n2.rename x y)
 
 /-- Renaming preserves size. -/
@@ -79,6 +70,28 @@ theorem Term.rename.eq_sizeOf {m : Term Var} {x y : Var} [DecidableEq Var] :
   sizeOf (m.rename x y) = sizeOf m := by
   induction m <;> aesop (add simp [Term.rename])
 
+open Term
+
+/-- α-equivalence. -/
+inductive Term.AlphaEquiv [DecidableEq Var] : Term Var → Term Var → Prop where
+| var {x} : AlphaEquiv (var x) (var x)
+| abs {y x1 x2 m1 m2} : y ≠ x1 → y ≠ x2 → y ∉ m1.vars → y ∉ m2.vars →
+  AlphaEquiv (m1.rename x1 y) (m2.rename x2 y) → AlphaEquiv (abs x1 m1) (abs x2 m2)
+| app {m1 n1 m2 n2} : AlphaEquiv m1 n1 → AlphaEquiv m2 n2 → AlphaEquiv (app m1 m2) (app n1 n2)
+
+/-- Instance for the notation `m =α n`. -/
+instance instHasAlphaEquivTerm [DecidableEq Var] : HasAlphaEquiv (Term Var) where
+  AlphaEquiv := Term.AlphaEquiv
+
+/-- Capture-avoiding substitution, as an inference system. -/
+inductive Term.Subst [DecidableEq Var] : Term Var → Var → Term Var → Term Var → Prop where
+  | varHit : (var x).Subst x r r
+  | varMiss : x ≠ y → (var y).Subst x r (var y)
+  | absShadow : (abs x m).Subst x r (abs x m)
+  | absIn : x ≠ y → y ∉ r.fv → m.Subst x r m' → (abs y m).Subst x r (abs y m')
+  | app : m.Subst x r m' → n.Subst x r n' → (app m n).Subst x r (app m' n')
+  | alpha : m =α m' → r =α r' → n =α n' → Subst m x r n → m'.Subst x r' n'
+
 /-- Capture-avoiding substitution. `m.subst x r` replaces the free occurrences of variable `x`
 in `m` with `r`. -/
 def Term.subst [DecidableEq Var] [HasFresh Var] (m : Term Var) (x : Var) (r : Term Var) :
@@ -102,15 +115,6 @@ instance instHasSubstitutionTerm [DecidableEq Var] [HasFresh Var] :
     HasSubstitution (Term Var) Var (Term Var) where
   subst := Term.subst
 
--- TODO
--- theorem Term.subst_comm
---   [DecidableEq Var] [HasFresh Var]
---   {m : Term Var} {x : Var} {n1 : Term Var} {y : Var} {n2 : Term Var} :
---   (m[x := n1])[y := n2] = (m[y := n2])[x := n1] := by
---   induction m
---   -- case var z =>
---   sorry
-
 /-- Contexts. -/
 inductive Context (Var : Type u) : Type u where
   | hole
@@ -127,39 +131,6 @@ def Context.fill (c : Context Var) (m : Term Var) : Term Var :=
   | appL c n => Term.app (c.fill m) n
   | appR n c => Term.app n (c.fill m)
 
-/-- Any `Term` can be obtained by filling a `Context` with a variable. This proves that `Context`
-completely captures the syntax of terms. -/
-theorem Context.complete (m : Term Var) :
-    ∃ (c : Context Var) (x : Var), m = (c.fill (Term.var x)) := by
-  induction m with
-  | var x => exists hole, x
-  | abs x n ih =>
-    obtain ⟨c', y, ih⟩ := ih
-    exists Context.abs x c', y
-    rw [ih, fill]
-  | app n₁ n₂ ih₁ ih₂ =>
-    obtain ⟨c₁, x₁, ih₁⟩ := ih₁
-    exists Context.appL c₁ n₂, x₁
-    rw [ih₁, fill]
-
-open Term
-
-/-- α-equivalence. -/
-inductive Term.AlphaEquiv [DecidableEq Var] : Term Var → Term Var → Prop where
--- The α-axiom
-| ax {m : Term Var} {x y : Var} :
-  y ∉ m.fv → AlphaEquiv (abs x m) (abs y (m.rename x y))
--- Equivalence relation rules
-| refl : AlphaEquiv m m
-| symm : AlphaEquiv m n → AlphaEquiv n m
-| trans : AlphaEquiv m1 m2 → AlphaEquiv m2 m3 → AlphaEquiv m1 m3
--- Context closure
-| ctx {c : Context Var} {m n : Term Var} : AlphaEquiv m n → AlphaEquiv (c.fill m) (c.fill n)
-
-/-- Instance for the notation `m =α n`. -/
-instance instHasAlphaEquivTerm [DecidableEq Var] : HasAlphaEquiv (Term Var) where
-  AlphaEquiv := Term.AlphaEquiv
-
 end LambdaCalculus.Named
 
 end Cslib

From 4d8d453e879cd7707c4189e7f9cedceae297d10c Mon Sep 17 00:00:00 2001
From: Haoxuan Yin <haoxn.yin@gmail.com>
Date: Tue, 10 Mar 2026 16:39:33 +0800
Subject: [PATCH 2/9] basic properties of renaming

---
 .../Named/Untyped/Properties.lean             | 58 +++++++++++++++++++
 1 file changed, 58 insertions(+)
 create mode 100644 Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean

diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
new file mode 100644
index 000000000..9fe1ca339
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2026 Haoxuan Yin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Haoxuan Yin
+-/
+
+module
+
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
+
+public section
+
+namespace Cslib
+
+universe u
+
+variable {Var : Type u}
+
+namespace LambdaCalculus.Named
+
+open Term
+
+/-- A variable in a term is either free or bound. -/
+lemma Term.vars_either_fv_or_bv [DecidableEq Var] (m : Term Var) :
+    m.vars = m.fv ∪ m.bv := by
+  induction m <;> grind [Term.fv, Term.bv, Term.vars]
+
+/-- Renaming an unused variable has no effect. -/
+lemma Term.rename_unused [DecidableEq Var] (m : Term Var) (x y : Var) :
+  x ∉ m.vars → m.rename x y = m := by
+  induction m <;> grind [Term.vars, Term.rename]
+
+/-- Renaming changes the set of variables. -/
+lemma Term.rename_vars [DecidableEq Var] (m : Term Var) (x y : Var) :
+  x ∈ m.vars → (m.rename x y).vars = m.vars.erase x ∪ {y} := by
+  induction m with
+  | var z => grind [Term.vars, Term.rename]
+  | abs z m ih =>
+    intro hx
+    by_cases hxm : x ∈ m.vars <;> grind [Term.vars, Term.rename, Term.rename_unused]
+  | app m n ihm ihn =>
+    intro hx
+    by_cases hxm : x ∈ m.vars
+    · by_cases hxn : x ∈ n.vars
+      · grind [Term.vars, Term.rename]
+      · grind [Term.vars, Term.rename, Term.rename_unused]
+    · have hxn : x ∈ n.vars := by
+        grind [Term.vars]
+      grind [Term.vars, Term.rename, Term.rename_unused]
+
+/-- Concatenation of renaming. -/
+lemma Term.rename_concat [DecidableEq Var] (m : Term Var) (x y z : Var) :
+  y ∉ m.vars → (m.rename x y).rename y z = m.rename x z := by
+  induction m <;> grind [Term.vars, Term.rename]
+
+end LambdaCalculus.Named
+
+end Cslib

From 8ade925e89ac562e22b3107f63858d428858dad4 Mon Sep 17 00:00:00 2001
From: Haoxuan Yin <haoxn.yin@gmail.com>
Date: Thu, 12 Mar 2026 11:26:44 +0800
Subject: [PATCH 3/9] properties of alpha equivalence

---
 .../LambdaCalculus/Named/Untyped/Basic.lean   |  16 +-
 .../Named/Untyped/Properties.lean             | 244 +++++++++++++++++-
 2 files changed, 238 insertions(+), 22 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
index a011f2270..8313e7734 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
@@ -60,7 +60,7 @@ def Term.vars [DecidableEq Var] : Term Var → Finset Var
     `m.rename x y` changes all occurrences of `x` into `y` in `m`. -/
 def Term.rename [DecidableEq Var] (m : Term Var) (x y : Var) : Term Var :=
   match m with
-  | var z => if z = x then (var y) else (var z)
+  | var z => var (if z = x then y else z)
   | abs z m' => abs (if z = x then y else z) (m'.rename x y)
   | app n1 n2 => app (n1.rename x y) (n2.rename x y)
 
@@ -75,7 +75,7 @@ open Term
 /-- α-equivalence. -/
 inductive Term.AlphaEquiv [DecidableEq Var] : Term Var → Term Var → Prop where
 | var {x} : AlphaEquiv (var x) (var x)
-| abs {y x1 x2 m1 m2} : y ≠ x1 → y ≠ x2 → y ∉ m1.vars → y ∉ m2.vars →
+| abs {y x1 x2 m1 m2} : y ∉ m1.vars ∪ m2.vars ∪ {x1, x2} →
   AlphaEquiv (m1.rename x1 y) (m2.rename x2 y) → AlphaEquiv (abs x1 m1) (abs x2 m2)
 | app {m1 n1 m2 n2} : AlphaEquiv m1 n1 → AlphaEquiv m2 n2 → AlphaEquiv (app m1 m2) (app n1 n2)
 
@@ -85,12 +85,12 @@ instance instHasAlphaEquivTerm [DecidableEq Var] : HasAlphaEquiv (Term Var) wher
 
 /-- Capture-avoiding substitution, as an inference system. -/
 inductive Term.Subst [DecidableEq Var] : Term Var → Var → Term Var → Term Var → Prop where
-  | varHit : (var x).Subst x r r
-  | varMiss : x ≠ y → (var y).Subst x r (var y)
-  | absShadow : (abs x m).Subst x r (abs x m)
-  | absIn : x ≠ y → y ∉ r.fv → m.Subst x r m' → (abs y m).Subst x r (abs y m')
-  | app : m.Subst x r m' → n.Subst x r n' → (app m n).Subst x r (app m' n')
-  | alpha : m =α m' → r =α r' → n =α n' → Subst m x r n → m'.Subst x r' n'
+  | varHit {x r} : (var x).Subst x r r
+  | varMiss {x y r} : x ≠ y → (var y).Subst x r (var y)
+  | absShadow {x m r} : (abs x m).Subst x r (abs x m)
+  | absIn {x y m r m'} : y ∉ r.fv ∪ {x} → m.Subst x r m' → (abs y m).Subst x r (abs y m')
+  | app {m n x r m' n'} : m.Subst x r m' → n.Subst x r n' → (app m n).Subst x r (app m' n')
+  | alpha {m m' r r' n n' x} : m =α m' → r =α r' → n =α n' → Subst m x r n → m'.Subst x r' n'
 
 /-- Capture-avoiding substitution. `m.subst x r` replaces the free occurrences of variable `x`
 in `m` with `r`. -/
diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
index 9fe1ca339..cc71ea415 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
@@ -21,37 +21,253 @@ namespace LambdaCalculus.Named
 open Term
 
 /-- A variable in a term is either free or bound. -/
-lemma Term.vars_either_fv_or_bv [DecidableEq Var] (m : Term Var) :
+lemma Term.vars_either_fv_or_bv [DecidableEq Var] {m : Term Var} :
     m.vars = m.fv ∪ m.bv := by
-  induction m <;> grind [Term.fv, Term.bv, Term.vars]
+  induction m <;> grind [fv, bv, vars]
 
 /-- Renaming an unused variable has no effect. -/
-lemma Term.rename_unused [DecidableEq Var] (m : Term Var) (x y : Var) :
+@[simp]
+lemma Term.rename_unused [DecidableEq Var] {m : Term Var} {x y : Var} :
   x ∉ m.vars → m.rename x y = m := by
-  induction m <;> grind [Term.vars, Term.rename]
+  induction m <;> grind [vars, rename]
 
-/-- Renaming changes the set of variables. -/
-lemma Term.rename_vars [DecidableEq Var] (m : Term Var) (x y : Var) :
+/-- Renaming a variable to itself has no effect. -/
+@[simp]
+lemma Term.rename_same [DecidableEq Var] {m : Term Var} {x : Var} :
+  m.rename x x = m := by
+  induction m <;> grind [vars, rename]
+
+/-- Renaming a used variable changes the set of variables. -/
+@[simp]
+lemma Term.rename_vars_used [DecidableEq Var] {m : Term Var} {x y : Var} :
   x ∈ m.vars → (m.rename x y).vars = m.vars.erase x ∪ {y} := by
   induction m with
-  | var z => grind [Term.vars, Term.rename]
+  | var z => grind [vars, rename]
   | abs z m ih =>
     intro hx
-    by_cases hxm : x ∈ m.vars <;> grind [Term.vars, Term.rename, Term.rename_unused]
+    by_cases hxm : x ∈ m.vars <;> grind [vars, rename, rename_unused]
   | app m n ihm ihn =>
     intro hx
     by_cases hxm : x ∈ m.vars
     · by_cases hxn : x ∈ n.vars
-      · grind [Term.vars, Term.rename]
-      · grind [Term.vars, Term.rename, Term.rename_unused]
+      · grind [vars, rename]
+      · grind [vars, rename, rename_unused]
     · have hxn : x ∈ n.vars := by
-        grind [Term.vars]
-      grind [Term.vars, Term.rename, Term.rename_unused]
+        grind [vars]
+      grind [vars, rename, rename_unused]
+
+/-- Renaming removes the variable. -/
+lemma Term.rename_remove [DecidableEq Var] {m : Term Var} {x y : Var} :
+  x ≠ y → x ∉ (m.rename x y).vars := by
+  intro hxy
+  by_cases hx : x ∈ m.vars <;> grind [rename_vars_used, rename_unused]
+
+/-- Renaming changes set of variables. -/
+lemma Term.rename_vars [DecidableEq Var] {m : Term Var} {x y : Var} :
+  (m.rename x y).vars ⊆ m.vars \ {x} ∪ {y} := by
+  by_cases x ∈ m.vars <;> grind [vars, rename, rename_unused, rename_vars_used]
 
 /-- Concatenation of renaming. -/
-lemma Term.rename_concat [DecidableEq Var] (m : Term Var) (x y z : Var) :
+@[simp]
+lemma Term.rename_concat [DecidableEq Var] {m : Term Var} {x y z : Var} :
   y ∉ m.vars → (m.rename x y).rename y z = m.rename x z := by
-  induction m <;> grind [Term.vars, Term.rename]
+  induction m <;> grind [vars, rename]
+
+/-- Commutativity of renaming. -/
+@[simp]
+lemma Term.rename_comm [DecidableEq Var] {m : Term Var} {x y z w : Var} :
+  x ≠ z → y ∉ m.vars ∪ {x, z} → w ∉ m.vars ∪ {x, z} →
+  (m.rename x y).rename z w = (m.rename z w).rename x y := by
+  induction m <;> grind [vars, rename]
+
+/-- α-equivalent terms have the same size. -/
+lemma AlphaEquiv.eq_sizeOf [DecidableEq Var] {m n : Term Var} :
+  m =α n → sizeOf m = sizeOf n := by
+  intro h
+  induction h with
+  | @var x => rfl
+  | @abs y x1 x2 m1 m2 hy h ih =>
+    simpa using ih
+  | @app m1 n1 m2 n2 _ hm hn =>
+    grind [app.sizeOf_spec]
+
+/-- Reflexivity of α-equivalence. -/
+lemma AlphaEquiv.refl [DecidableEq Var] [HasFresh Var] (m : Term Var) : m =α m := by
+  refine WellFounded.induction (C := fun m => m =α m) sizeOfWFRel.wf m ?_
+  simp only; intro m ih
+  cases m with
+  | var x => apply AlphaEquiv.var
+  | abs x m =>
+    obtain ⟨z, hz⟩ := HasFresh.fresh_exists (m.vars ∪ {x})
+    apply AlphaEquiv.abs (y := z) (x1 := x) (x2 := x) (m1 := m) (m2 := m)
+    <;> try grind [rename_unused, rename_vars, rename_concat]
+    · apply ih
+      change sizeOf (m.rename x z) < sizeOf (abs x m)
+      grind [rename.eq_sizeOf, abs.sizeOf_spec]
+  | app m n =>
+    apply AlphaEquiv.app
+    · apply ih
+      change sizeOf m < sizeOf (app m n)
+      grind [rename.eq_sizeOf, app.sizeOf_spec]
+    · apply ih
+      change sizeOf n < sizeOf (app m n)
+      grind [rename.eq_sizeOf, app.sizeOf_spec]
+
+/-- Symmetry of α-equivalence. -/
+lemma AlphaEquiv.symm [DecidableEq Var] [HasFresh Var] {m n : Term Var} :
+  m =α n → n =α m := by
+  intro h
+  induction h with
+  | @var x => apply AlphaEquiv.var
+  | @abs y x1 x2 m1 m2 hy h ih =>
+    apply AlphaEquiv.abs (y := y) (x1 := x2) (x2 := x1) (m1 := m2) (m2 := m1)
+    <;> try grind [rename_unused, rename_vars, rename_concat]
+    · apply ih
+  | @app m1 n1 m2 n2 hwm1 hwn1 hwm2 hwn2 =>
+    apply AlphaEquiv.app <;> assumption
+
+/-- Renaming under an abstraction body can be reordered against the outer renaming.
+    This lemma is used for the lemma below. -/
+lemma Term.rename_abs_body_comm [DecidableEq Var] {m : Term Var} {x y z w : Var} :
+  y ∉ m.vars ∪ {x, z} → w ∉ m.vars ∪ {x, y, z} →
+  (m.rename x y).rename (if z = x then y else z) w = (m.rename z w).rename x y := by
+  intro hy hw
+  by_cases hzx : z = x
+  · grind [rename_same, rename_unused, rename_concat, rename_vars]
+  · grind [rename_comm]
+
+/-- Renaming α-equivalent terms produces α-equivalent terms. -/
+lemma AlphaEquiv.rename_preserve [DecidableEq Var] [HasFresh Var]
+  (m n : Term Var) (x y : Var) :
+  y ∉ m.vars ∪ n.vars → m =α n → (m.rename x y) =α (n.rename x y) := by
+  refine (WellFounded.induction sizeOfWFRel.wf m
+    (C := fun m => ∀ (n : Term Var) (x y : Var), y ∉ m.vars ∪ n.vars →
+      m =α n → (m.rename x y) =α (n.rename x y)) ?_) n x y
+  intro m ih n x y hy h
+  by_cases hxy : y = x
+  · grind [rename_same]
+  cases h with
+  | @var z => apply AlphaEquiv.refl
+  | @abs z x1 x2 m1 m2 hz hbody =>
+    obtain ⟨w, hw⟩ := HasFresh.fresh_exists (m1.vars ∪ m2.vars ∪ {x1, x2, x, y, z})
+    apply AlphaEquiv.abs (y := w) <;> try grind [rename_vars]
+    rw [rename_abs_body_comm, rename_abs_body_comm] <;> try grind [vars]
+    apply ih <;> try grind [vars, rename_vars]
+    · change sizeOf (m1.rename x1 w) < sizeOf (abs x1 m1)
+      grind [rename.eq_sizeOf, abs.sizeOf_spec]
+    · have hxzw : ((m1.rename x1 z).rename z w) =α ((m2.rename x2 z).rename z w) := by
+        apply ih <;> try grind [vars, rename_vars]
+        · change sizeOf (m1.rename x1 z) < sizeOf (abs x1 m1)
+          grind [rename.eq_sizeOf, abs.sizeOf_spec]
+        · assumption
+      grind [rename_concat]
+  | @app m1 n1 m2 n2 hm hn =>
+    apply AlphaEquiv.app
+    · apply ih m1 <;> try grind [vars]
+      · change sizeOf m1 < sizeOf (app m1 m2)
+        grind [app.sizeOf_spec]
+      · assumption
+    · apply ih m2 <;> try grind [vars]
+      · change sizeOf m2 < sizeOf (app m1 m2)
+        grind [app.sizeOf_spec]
+      · assumption
+
+/-- Elimination rule for α-equivalence of abstractions.
+    It states that if two abstractions are α-equivalent,
+    then their bodies can be renamed to ``any'' fresh variable y and remain α-equivalent.
+    This is sometimes easier to use than using by_cases on the equivalence,
+    which can only produce the claim for ``some'' fresh y. -/
+lemma AlphaEquiv.abs_elim [DecidableEq Var] [HasFresh Var] {m1 m2 : Term Var} {x1 x2 y : Var} :
+  y ∉ m1.vars ∪ m2.vars ∪ {x1, x2} → (abs x1 m1) =α (abs x2 m2) →
+  (m1.rename x1 y) =α (m2.rename x2 y) := by
+  intro hy h
+  cases h with
+  | @abs z _ _ _ _ hz h1 =>
+    by_cases hzy : z = y
+    · subst z
+      assumption
+    · have hxzy : ((m1.rename x1 z).rename z y) =α ((m2.rename x2 z).rename z y) := by
+        apply AlphaEquiv.rename_preserve <;> try grind [AlphaEquiv.rename_preserve, rename_vars]
+        assumption
+      grind [rename_concat, rename_vars]
+
+/-- Transitivity of α-equivalence. -/
+lemma AlphaEquiv.trans [DecidableEq Var] [HasFresh Var] {m n p : Term Var} :
+  m =α n → n =α p → m =α p := by
+  refine (WellFounded.induction sizeOfWFRel.wf m
+    (C := fun m => ∀ (n p : Term Var),
+      m =α n → n =α p → m =α p) ?_) n p
+  intro m ih n p hmn hnp
+  cases m with
+  | var x =>
+    cases hmn with
+    | @var x => assumption
+  | abs x1 m1 =>
+    obtain ⟨w, hw⟩ := HasFresh.fresh_exists (m1.vars ∪ {x1} ∪ n.vars ∪ p.vars)
+    have hmn' := hmn
+    cases hmn' with
+    | @abs y x1 x2 m1 m2 hy h1 =>
+      have hnp' := hnp
+      cases hnp' with
+      | @abs z x2 x3 m2 m3 hz h2 =>
+        apply AlphaEquiv.abs (y := w)
+        <;> try grind [vars, rename_unused, rename_vars, rename_concat]
+        · apply ih _ ?_ (m2.rename x2 w) <;> try grind [AlphaEquiv.abs_elim, vars, rename_vars]
+          change sizeOf (m1.rename x1 w) < sizeOf (abs x1 m1)
+          grind [rename.eq_sizeOf, abs.sizeOf_spec]
+  | app m1 m2 =>
+    cases hmn with
+    | @app m1 n1 m2 n2 hmn1 hmn2 =>
+      cases hnp with
+      | @app n1 p1 n2 p2 hnp1 hnp2 =>
+        apply AlphaEquiv.app
+        · apply ih _ ?_ n1 <;> try assumption; try grind [vars, rename_vars]
+          change sizeOf m1 < sizeOf (app m1 m2)
+          grind [app.sizeOf_spec]
+        · apply ih _ ?_ n2 <;> try assumption; try grind [vars, rename_vars]
+          change sizeOf m2 < sizeOf (app m1 m2)
+          grind [app.sizeOf_spec]
+
+/-- Renaming a non-free variable result in an α-equivalent term. -/
+lemma AlphaEquiv.rename_non_fv [DecidableEq Var] [HasFresh Var] (m : Term Var) (x y : Var)
+  (hxm : x ∉ m.fv) (hym : y ∉ m.vars) : m =α (m.rename x y) := by
+  induction m with
+  | var z =>
+    have hzx : z ≠ x := by
+      grind [fv]
+    simpa [rename, hzx] using AlphaEquiv.var
+  | abs z m ih =>
+    by_cases hzx : z = x
+    · subst z
+      simp only [rename, ↓reduceIte]
+      obtain ⟨w, hw⟩ := HasFresh.fresh_exists (m.vars ∪ {x, y})
+      apply AlphaEquiv.abs (y := w)<;> try grind [rename_unused, rename_vars]
+      rw [rename_concat] <;> try grind [vars]
+      apply AlphaEquiv.refl
+    · simp only [rename, hzx, ↓reduceIte]
+      obtain ⟨w, hw⟩ := HasFresh.fresh_exists (m.vars ∪ {x, y, z})
+      apply AlphaEquiv.abs (y := w) <;> try grind [rename_unused, rename_vars]
+      apply AlphaEquiv.rename_preserve <;> grind [vars, rename_vars, fv]
+  | app m1 m2 ih1 ih2 =>
+    apply AlphaEquiv.app
+    · apply ih1 <;> grind [vars, fv]
+    · apply ih2 <;> grind [vars, fv]
+
+/-- Any `Term` can be obtained by filling a `Context` with a variable. This proves that `Context`
+completely captures the syntax of terms. -/
+theorem Context.complete (m : Term Var) :
+    ∃ (c : Context Var) (x : Var), m = (c.fill (Term.var x)) := by
+  induction m with
+  | var x => exists hole, x
+  | abs x n ih =>
+    obtain ⟨c', y, ih⟩ := ih
+    exists Context.abs x c', y
+    rw [ih, fill]
+  | app n₁ n₂ ih₁ ih₂ =>
+    obtain ⟨c₁, x₁, ih₁⟩ := ih₁
+    exists Context.appL c₁ n₂, x₁
+    rw [ih₁, fill]
+
 
 end LambdaCalculus.Named
 

From a670c7125970760081afa02d4fac8a09cd7b8b06 Mon Sep 17 00:00:00 2001
From: Haoxuan Yin <haoxn.yin@gmail.com>
Date: Sat, 21 Mar 2026 09:55:57 +0000
Subject: [PATCH 4/9] allow grind to recognise notation of alpha-equivalence

---
 .../LambdaCalculus/Named/Untyped/Basic.lean   |  5 +++++
 .../Named/Untyped/Properties.lean             | 19 ++++++-------------
 2 files changed, 11 insertions(+), 13 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
index 8313e7734..472bc653a 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
@@ -83,6 +83,11 @@ inductive Term.AlphaEquiv [DecidableEq Var] : Term Var → Term Var → Prop whe
 instance instHasAlphaEquivTerm [DecidableEq Var] : HasAlphaEquiv (Term Var) where
   AlphaEquiv := Term.AlphaEquiv
 
+/-- Allow grind to recognise the notation of α-equivalence. -/
+@[grind ←]
+theorem Term.AlphaEquiv_def [DecidableEq Var] (m n : Term Var) :
+  AlphaEquiv m n ↔ m =α n := by rfl
+
 /-- Capture-avoiding substitution, as an inference system. -/
 inductive Term.Subst [DecidableEq Var] : Term Var → Var → Term Var → Term Var → Prop where
   | varHit {x r} : (var x).Subst x r r
diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
index cc71ea415..6d9d0dac7 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
@@ -99,7 +99,7 @@ lemma AlphaEquiv.refl [DecidableEq Var] [HasFresh Var] (m : Term Var) : m =α m
   | var x => apply AlphaEquiv.var
   | abs x m =>
     obtain ⟨z, hz⟩ := HasFresh.fresh_exists (m.vars ∪ {x})
-    apply AlphaEquiv.abs (y := z) (x1 := x) (x2 := x) (m1 := m) (m2 := m)
+    apply AlphaEquiv.abs (y := z)
     <;> try grind [rename_unused, rename_vars, rename_concat]
     · apply ih
       change sizeOf (m.rename x z) < sizeOf (abs x m)
@@ -120,9 +120,7 @@ lemma AlphaEquiv.symm [DecidableEq Var] [HasFresh Var] {m n : Term Var} :
   induction h with
   | @var x => apply AlphaEquiv.var
   | @abs y x1 x2 m1 m2 hy h ih =>
-    apply AlphaEquiv.abs (y := y) (x1 := x2) (x2 := x1) (m1 := m2) (m2 := m1)
-    <;> try grind [rename_unused, rename_vars, rename_concat]
-    · apply ih
+    apply AlphaEquiv.abs (y := y) <;> grind [rename_unused, rename_vars, rename_concat]
   | @app m1 n1 m2 n2 hwm1 hwn1 hwm2 hwn2 =>
     apply AlphaEquiv.app <;> assumption
 
@@ -159,18 +157,15 @@ lemma AlphaEquiv.rename_preserve [DecidableEq Var] [HasFresh Var]
         apply ih <;> try grind [vars, rename_vars]
         · change sizeOf (m1.rename x1 z) < sizeOf (abs x1 m1)
           grind [rename.eq_sizeOf, abs.sizeOf_spec]
-        · assumption
       grind [rename_concat]
   | @app m1 n1 m2 n2 hm hn =>
     apply AlphaEquiv.app
     · apply ih m1 <;> try grind [vars]
       · change sizeOf m1 < sizeOf (app m1 m2)
         grind [app.sizeOf_spec]
-      · assumption
     · apply ih m2 <;> try grind [vars]
       · change sizeOf m2 < sizeOf (app m1 m2)
         grind [app.sizeOf_spec]
-      · assumption
 
 /-- Elimination rule for α-equivalence of abstractions.
     It states that if two abstractions are α-equivalent,
@@ -184,11 +179,9 @@ lemma AlphaEquiv.abs_elim [DecidableEq Var] [HasFresh Var] {m1 m2 : Term Var} {x
   cases h with
   | @abs z _ _ _ _ hz h1 =>
     by_cases hzy : z = y
-    · subst z
-      assumption
+    · grind
     · have hxzy : ((m1.rename x1 z).rename z y) =α ((m2.rename x2 z).rename z y) := by
-        apply AlphaEquiv.rename_preserve <;> try grind [AlphaEquiv.rename_preserve, rename_vars]
-        assumption
+        apply AlphaEquiv.rename_preserve <;> grind [AlphaEquiv.rename_preserve, rename_vars]
       grind [rename_concat, rename_vars]
 
 /-- Transitivity of α-equivalence. -/
@@ -221,10 +214,10 @@ lemma AlphaEquiv.trans [DecidableEq Var] [HasFresh Var] {m n p : Term Var} :
       cases hnp with
       | @app n1 p1 n2 p2 hnp1 hnp2 =>
         apply AlphaEquiv.app
-        · apply ih _ ?_ n1 <;> try assumption; try grind [vars, rename_vars]
+        · apply ih _ ?_ n1 <;> try grind [vars, rename_vars]
           change sizeOf m1 < sizeOf (app m1 m2)
           grind [app.sizeOf_spec]
-        · apply ih _ ?_ n2 <;> try assumption; try grind [vars, rename_vars]
+        · apply ih _ ?_ n2 <;> try grind [vars, rename_vars]
           change sizeOf m2 < sizeOf (app m1 m2)
           grind [app.sizeOf_spec]
 

From 510675f0ce7bf4a70fd998c5276c6d29b286264f Mon Sep 17 00:00:00 2001
From: Haoxuan Yin <haoxn.yin@gmail.com>
Date: Wed, 25 Mar 2026 14:54:57 +0000
Subject: [PATCH 5/9] Properties of substitution: equivalence between
 functional and relational definitions

---
 .../LambdaCalculus/Named/Untyped/Basic.lean   |  23 +-
 .../Named/Untyped/Properties.lean             | 481 +++++++++++++++---
 2 files changed, 425 insertions(+), 79 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
index 472bc653a..6ee9b4ce6 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
@@ -19,7 +19,8 @@ The untyped λ-calculus.
 ## References
 
 * [H. Barendregt, *Introduction to Lambda Calculus*][Barendregt1984]
-* Definition of α-equivalence [A. Pitts, *Nominal Techniques*][Pitts2015]
+* Definition of α-equivalence [M. Gabbay and A. Pitts, *A New Approach to Abstract Syntax with
+Variable Binding*][Gabbay2002]
 
 -/
 
@@ -41,13 +42,13 @@ deriving DecidableEq
 /-- Free variables. -/
 def Term.fv [DecidableEq Var] : Term Var → Finset Var
   | var x => {x}
-  | abs x m => m.fv.erase x
+  | abs x m => m.fv \ {x}
   | app m n => m.fv ∪ n.fv
 
 /-- Bound variables. -/
 def Term.bv [DecidableEq Var] : Term Var → Finset Var
   | var _ => ∅
-  | abs x m => m.bv ∪ {x} -- Could also be `insert x m.bv`
+  | abs x m => m.bv ∪ {x}
   | app m n => m.bv ∪ n.bv
 
 /-- Variable names (free and bound) in a term. -/
@@ -91,7 +92,7 @@ theorem Term.AlphaEquiv_def [DecidableEq Var] (m n : Term Var) :
 /-- Capture-avoiding substitution, as an inference system. -/
 inductive Term.Subst [DecidableEq Var] : Term Var → Var → Term Var → Term Var → Prop where
   | varHit {x r} : (var x).Subst x r r
-  | varMiss {x y r} : x ≠ y → (var y).Subst x r (var y)
+  | varMiss {x y r} : y ≠ x → (var y).Subst x r (var y)
   | absShadow {x m r} : (abs x m).Subst x r (abs x m)
   | absIn {x y m r m'} : y ∉ r.fv ∪ {x} → m.Subst x r m' → (abs y m).Subst x r (abs y m')
   | app {m n x r m' n'} : m.Subst x r m' → n.Subst x r n' → (app m n).Subst x r (app m' n')
@@ -99,6 +100,7 @@ inductive Term.Subst [DecidableEq Var] : Term Var → Var → Term Var → Term
 
 /-- Capture-avoiding substitution. `m.subst x r` replaces the free occurrences of variable `x`
 in `m` with `r`. -/
+@[grind, simp]
 def Term.subst [DecidableEq Var] [HasFresh Var] (m : Term Var) (x : Var) (r : Term Var) :
   Term Var :=
   match m with
@@ -109,7 +111,7 @@ def Term.subst [DecidableEq Var] [HasFresh Var] (m : Term Var) (x : Var) (r : Te
     else if y ∉ r.fv then
       abs y (m'.subst x r)
     else
-      let z := HasFresh.fresh (m'.vars ∪ r.vars ∪ {x})
+      let z := HasFresh.fresh (m'.vars ∪ r.vars ∪ {x, y})
       abs z ((m'.rename y z).subst x r)
   | app m1 m2 => app (m1.subst x r) (m2.subst x r)
 termination_by m
@@ -120,6 +122,11 @@ instance instHasSubstitutionTerm [DecidableEq Var] [HasFresh Var] :
     HasSubstitution (Term Var) Var (Term Var) where
   subst := Term.subst
 
+/-- Allow grind to recognise the notation of substitution. -/
+@[grind ←, simp← ]
+theorem Term.subst_def [DecidableEq Var] (m r : Term Var) (x : Var) [HasFresh Var] :
+  m.subst x r = m[x := r] := by rfl
+
 /-- Contexts. -/
 inductive Context (Var : Type u) : Type u where
   | hole
@@ -136,6 +143,12 @@ def Context.fill (c : Context Var) (m : Term Var) : Term Var :=
   | appL c n => Term.app (c.fill m) n
   | appR n c => Term.app n (c.fill m)
 
+def Context.vars [DecidableEq Var] : Context Var → Finset Var
+  | hole => ∅
+  | abs x c => c.vars ∪ {x}
+  | appL c m => c.vars ∪ m.vars
+  | appR m c => m.vars ∪ c.vars
+
 end LambdaCalculus.Named
 
 end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
index 6d9d0dac7..ce471e785 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2026 Haoxuan Yin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Haoxuan Yin
+Authors: Haoxuan Yin, Fabrizio Montesi
 -/
 
 module
@@ -21,25 +21,25 @@ namespace LambdaCalculus.Named
 open Term
 
 /-- A variable in a term is either free or bound. -/
-lemma Term.vars_either_fv_or_bv [DecidableEq Var] {m : Term Var} :
+theorem vars_either_fv_or_bv [DecidableEq Var] {m : Term Var} :
     m.vars = m.fv ∪ m.bv := by
   induction m <;> grind [fv, bv, vars]
 
 /-- Renaming an unused variable has no effect. -/
 @[simp]
-lemma Term.rename_unused [DecidableEq Var] {m : Term Var} {x y : Var} :
+theorem rename_unused [DecidableEq Var] {m : Term Var} {x y : Var} :
   x ∉ m.vars → m.rename x y = m := by
   induction m <;> grind [vars, rename]
 
 /-- Renaming a variable to itself has no effect. -/
 @[simp]
-lemma Term.rename_same [DecidableEq Var] {m : Term Var} {x : Var} :
+theorem rename_same [DecidableEq Var] {m : Term Var} {x : Var} :
   m.rename x x = m := by
   induction m <;> grind [vars, rename]
 
 /-- Renaming a used variable changes the set of variables. -/
 @[simp]
-lemma Term.rename_vars_used [DecidableEq Var] {m : Term Var} {x y : Var} :
+theorem rename_vars_used [DecidableEq Var] {m : Term Var} {x y : Var} :
   x ∈ m.vars → (m.rename x y).vars = m.vars.erase x ∪ {y} := by
   induction m with
   | var z => grind [vars, rename]
@@ -49,39 +49,46 @@ lemma Term.rename_vars_used [DecidableEq Var] {m : Term Var} {x y : Var} :
   | app m n ihm ihn =>
     intro hx
     by_cases hxm : x ∈ m.vars
-    · by_cases hxn : x ∈ n.vars
-      · grind [vars, rename]
-      · grind [vars, rename, rename_unused]
-    · have hxn : x ∈ n.vars := by
-        grind [vars]
+    · by_cases hxn : x ∈ n.vars <;> grind [vars, rename, rename_unused]
+    · have hxn : x ∈ n.vars := by grind [vars]
       grind [vars, rename, rename_unused]
 
 /-- Renaming removes the variable. -/
-lemma Term.rename_remove [DecidableEq Var] {m : Term Var} {x y : Var} :
+theorem rename_remove [DecidableEq Var] {m : Term Var} {x y : Var} :
   x ≠ y → x ∉ (m.rename x y).vars := by
   intro hxy
   by_cases hx : x ∈ m.vars <;> grind [rename_vars_used, rename_unused]
 
-/-- Renaming changes set of variables. -/
-lemma Term.rename_vars [DecidableEq Var] {m : Term Var} {x y : Var} :
-  (m.rename x y).vars ⊆ m.vars \ {x} ∪ {y} := by
+/-- The set of variables after renaming. -/
+theorem rename_vars [DecidableEq Var] {m : Term Var} {x y : Var} :
+  (m.rename x y).vars = m.vars \ {x} ∪ (if x ∈ m.vars then {y} else ∅) := by
   by_cases x ∈ m.vars <;> grind [vars, rename, rename_unused, rename_vars_used]
 
+/-- The set of free variables after renaming. -/
+theorem rename_fv [DecidableEq Var] {m : Term Var} {x y : Var} :
+  y ∉ m.vars → (m.rename x y).fv = m.fv \ {x} ∪ (if x ∈ m.fv then {y} else ∅) := by
+  induction m <;> grind [fv, vars, rename, vars_either_fv_or_bv]
+
 /-- Concatenation of renaming. -/
 @[simp]
-lemma Term.rename_concat [DecidableEq Var] {m : Term Var} {x y z : Var} :
+theorem rename_concat [DecidableEq Var] {m : Term Var} {x y z : Var} :
   y ∉ m.vars → (m.rename x y).rename y z = m.rename x z := by
   induction m <;> grind [vars, rename]
 
 /-- Commutativity of renaming. -/
-@[simp]
-lemma Term.rename_comm [DecidableEq Var] {m : Term Var} {x y z w : Var} :
+theorem rename_comm [DecidableEq Var] {m : Term Var} {x y z w : Var} :
   x ≠ z → y ∉ m.vars ∪ {x, z} → w ∉ m.vars ∪ {x, z} →
   (m.rename x y).rename z w = (m.rename z w).rename x y := by
   induction m <;> grind [vars, rename]
 
+@[grind ←]
+lemma induction_by_sizeOf {m n : Term Var} :
+  WellFoundedRelation.rel m n ↔
+  sizeOf m < sizeOf n := by
+  rfl
+
 /-- α-equivalent terms have the same size. -/
-lemma AlphaEquiv.eq_sizeOf [DecidableEq Var] {m n : Term Var} :
+theorem AlphaEquiv.eq_sizeOf [DecidableEq Var] {m n : Term Var} :
   m =α n → sizeOf m = sizeOf n := by
   intro h
   induction h with
@@ -89,10 +96,25 @@ lemma AlphaEquiv.eq_sizeOf [DecidableEq Var] {m n : Term Var} :
   | @abs y x1 x2 m1 m2 hy h ih =>
     simpa using ih
   | @app m1 n1 m2 n2 _ hm hn =>
-    grind [app.sizeOf_spec]
+    grind
+
+/-- α-equivalent terms have the same free variables. -/
+theorem AlphaEquiv.same_fv [DecidableEq Var] {m n : Term Var} :
+  m =α n → m.fv = n.fv := by
+  intro h
+  induction h with
+  | @var x => rfl
+  | @abs y x1 x2 m1 m2 hy h ih =>
+    rw [Term.fv, Term.fv]
+    have h1 : m1.fv \ {x1} = (m1.rename x1 y).fv \ {y} := by
+      grind [rename_fv, vars_either_fv_or_bv]
+    have h2 : (m2.rename x2 y).fv \ {y} = m2.fv \ {x2} := by
+      grind [rename_fv, vars_either_fv_or_bv]
+    grind
+  | @app m1 n1 m2 n2 h1 h2 ih1 ih2 => grind [Term.fv]
 
 /-- Reflexivity of α-equivalence. -/
-lemma AlphaEquiv.refl [DecidableEq Var] [HasFresh Var] (m : Term Var) : m =α m := by
+theorem AlphaEquiv.refl [DecidableEq Var] [HasFresh Var] (m : Term Var) : m =α m := by
   refine WellFounded.induction (C := fun m => m =α m) sizeOfWFRel.wf m ?_
   simp only; intro m ih
   cases m with
@@ -100,21 +122,14 @@ lemma AlphaEquiv.refl [DecidableEq Var] [HasFresh Var] (m : Term Var) : m =α m
   | abs x m =>
     obtain ⟨z, hz⟩ := HasFresh.fresh_exists (m.vars ∪ {x})
     apply AlphaEquiv.abs (y := z)
-    <;> try grind [rename_unused, rename_vars, rename_concat]
-    · apply ih
-      change sizeOf (m.rename x z) < sizeOf (abs x m)
-      grind [rename.eq_sizeOf, abs.sizeOf_spec]
+    · grind [rename_vars]
+    apply ih
+    grind [rename.eq_sizeOf]
   | app m n =>
-    apply AlphaEquiv.app
-    · apply ih
-      change sizeOf m < sizeOf (app m n)
-      grind [rename.eq_sizeOf, app.sizeOf_spec]
-    · apply ih
-      change sizeOf n < sizeOf (app m n)
-      grind [rename.eq_sizeOf, app.sizeOf_spec]
+    apply AlphaEquiv.app <;> apply ih <;> grind
 
 /-- Symmetry of α-equivalence. -/
-lemma AlphaEquiv.symm [DecidableEq Var] [HasFresh Var] {m n : Term Var} :
+theorem AlphaEquiv.symm [DecidableEq Var] [HasFresh Var] {m n : Term Var} :
   m =α n → n =α m := by
   intro h
   induction h with
@@ -124,9 +139,8 @@ lemma AlphaEquiv.symm [DecidableEq Var] [HasFresh Var] {m n : Term Var} :
   | @app m1 n1 m2 n2 hwm1 hwn1 hwm2 hwn2 =>
     apply AlphaEquiv.app <;> assumption
 
-/-- Renaming under an abstraction body can be reordered against the outer renaming.
-    This lemma is used for the lemma below. -/
-lemma Term.rename_abs_body_comm [DecidableEq Var] {m : Term Var} {x y z w : Var} :
+/-- Commutativity of renaming, more general version. -/
+theorem rename_comm2 [DecidableEq Var] {m : Term Var} {x y z w : Var} :
   y ∉ m.vars ∪ {x, z} → w ∉ m.vars ∪ {x, y, z} →
   (m.rename x y).rename (if z = x then y else z) w = (m.rename z w).rename x y := by
   intro hy hw
@@ -135,44 +149,39 @@ lemma Term.rename_abs_body_comm [DecidableEq Var] {m : Term Var} {x y z w : Var}
   · grind [rename_comm]
 
 /-- Renaming α-equivalent terms produces α-equivalent terms. -/
-lemma AlphaEquiv.rename_preserve [DecidableEq Var] [HasFresh Var]
+theorem AlphaEquiv.rename_preserve [DecidableEq Var] [HasFresh Var]
   (m n : Term Var) (x y : Var) :
   y ∉ m.vars ∪ n.vars → m =α n → (m.rename x y) =α (n.rename x y) := by
   refine (WellFounded.induction sizeOfWFRel.wf m
     (C := fun m => ∀ (n : Term Var) (x y : Var), y ∉ m.vars ∪ n.vars →
       m =α n → (m.rename x y) =α (n.rename x y)) ?_) n x y
   intro m ih n x y hy h
-  by_cases hxy : y = x
+  by_cases hyx : y = x
   · grind [rename_same]
   cases h with
   | @var z => apply AlphaEquiv.refl
   | @abs z x1 x2 m1 m2 hz hbody =>
     obtain ⟨w, hw⟩ := HasFresh.fresh_exists (m1.vars ∪ m2.vars ∪ {x1, x2, x, y, z})
-    apply AlphaEquiv.abs (y := w) <;> try grind [rename_vars]
-    rw [rename_abs_body_comm, rename_abs_body_comm] <;> try grind [vars]
-    apply ih <;> try grind [vars, rename_vars]
-    · change sizeOf (m1.rename x1 w) < sizeOf (abs x1 m1)
-      grind [rename.eq_sizeOf, abs.sizeOf_spec]
-    · have hxzw : ((m1.rename x1 z).rename z w) =α ((m2.rename x2 z).rename z w) := by
-        apply ih <;> try grind [vars, rename_vars]
-        · change sizeOf (m1.rename x1 z) < sizeOf (abs x1 m1)
-          grind [rename.eq_sizeOf, abs.sizeOf_spec]
-      grind [rename_concat]
+    apply AlphaEquiv.abs (y := w)
+    · grind [rename_vars]
+    rw [rename_comm2, rename_comm2]
+    case neg.abs.a =>
+      apply ih
+      · grind [rename.eq_sizeOf]
+      · grind [vars, rename_vars]
+      · have hxzw : ((m1.rename x1 z).rename z w) =α ((m2.rename x2 z).rename z w) := by
+          apply ih <;> grind [vars, rename_vars, rename.eq_sizeOf]
+        grind [rename_concat]
+    all_goals grind [vars]
   | @app m1 n1 m2 n2 hm hn =>
-    apply AlphaEquiv.app
-    · apply ih m1 <;> try grind [vars]
-      · change sizeOf m1 < sizeOf (app m1 m2)
-        grind [app.sizeOf_spec]
-    · apply ih m2 <;> try grind [vars]
-      · change sizeOf m2 < sizeOf (app m1 m2)
-        grind [app.sizeOf_spec]
+    apply AlphaEquiv.app <;> apply ih <;> grind [vars]
 
 /-- Elimination rule for α-equivalence of abstractions.
     It states that if two abstractions are α-equivalent,
     then their bodies can be renamed to ``any'' fresh variable y and remain α-equivalent.
     This is sometimes easier to use than using by_cases on the equivalence,
     which can only produce the claim for ``some'' fresh y. -/
-lemma AlphaEquiv.abs_elim [DecidableEq Var] [HasFresh Var] {m1 m2 : Term Var} {x1 x2 y : Var} :
+theorem AlphaEquiv.abs_elim [DecidableEq Var] [HasFresh Var] {m1 m2 : Term Var} {x1 x2 y : Var} :
   y ∉ m1.vars ∪ m2.vars ∪ {x1, x2} → (abs x1 m1) =α (abs x2 m2) →
   (m1.rename x1 y) =α (m2.rename x2 y) := by
   intro hy h
@@ -185,7 +194,7 @@ lemma AlphaEquiv.abs_elim [DecidableEq Var] [HasFresh Var] {m1 m2 : Term Var} {x
       grind [rename_concat, rename_vars]
 
 /-- Transitivity of α-equivalence. -/
-lemma AlphaEquiv.trans [DecidableEq Var] [HasFresh Var] {m n p : Term Var} :
+theorem AlphaEquiv.trans [DecidableEq Var] [HasFresh Var] {m n p : Term Var} :
   m =α n → n =α p → m =α p := by
   refine (WellFounded.induction sizeOfWFRel.wf m
     (C := fun m => ∀ (n p : Term Var),
@@ -204,25 +213,20 @@ lemma AlphaEquiv.trans [DecidableEq Var] [HasFresh Var] {m n p : Term Var} :
       cases hnp' with
       | @abs z x2 x3 m2 m3 hz h2 =>
         apply AlphaEquiv.abs (y := w)
-        <;> try grind [vars, rename_unused, rename_vars, rename_concat]
-        · apply ih _ ?_ (m2.rename x2 w) <;> try grind [AlphaEquiv.abs_elim, vars, rename_vars]
-          change sizeOf (m1.rename x1 w) < sizeOf (abs x1 m1)
-          grind [rename.eq_sizeOf, abs.sizeOf_spec]
+        · grind [vars, rename_unused, rename_vars, rename_concat]
+        apply ih _ ?_ (m2.rename x2 w) <;>
+        grind [AlphaEquiv.abs_elim, vars, rename_vars, rename.eq_sizeOf]
   | app m1 m2 =>
     cases hmn with
     | @app m1 n1 m2 n2 hmn1 hmn2 =>
       cases hnp with
       | @app n1 p1 n2 p2 hnp1 hnp2 =>
         apply AlphaEquiv.app
-        · apply ih _ ?_ n1 <;> try grind [vars, rename_vars]
-          change sizeOf m1 < sizeOf (app m1 m2)
-          grind [app.sizeOf_spec]
-        · apply ih _ ?_ n2 <;> try grind [vars, rename_vars]
-          change sizeOf m2 < sizeOf (app m1 m2)
-          grind [app.sizeOf_spec]
-
-/-- Renaming a non-free variable result in an α-equivalent term. -/
-lemma AlphaEquiv.rename_non_fv [DecidableEq Var] [HasFresh Var] (m : Term Var) (x y : Var)
+        · apply ih _ ?_ n1 <;> grind [vars, rename_vars]
+        · apply ih _ ?_ n2 <;> grind [vars, rename_vars]
+
+/-- Renaming a non-free variable result in an α-equivalent term -/
+theorem AlphaEquiv.rename_non_fv [DecidableEq Var] [HasFresh Var] (m : Term Var) (x y : Var)
   (hxm : x ∉ m.fv) (hym : y ∉ m.vars) : m =α (m.rename x y) := by
   induction m with
   | var z =>
@@ -234,22 +238,34 @@ lemma AlphaEquiv.rename_non_fv [DecidableEq Var] [HasFresh Var] (m : Term Var) (
     · subst z
       simp only [rename, ↓reduceIte]
       obtain ⟨w, hw⟩ := HasFresh.fresh_exists (m.vars ∪ {x, y})
-      apply AlphaEquiv.abs (y := w)<;> try grind [rename_unused, rename_vars]
-      rw [rename_concat] <;> try grind [vars]
-      apply AlphaEquiv.refl
+      apply AlphaEquiv.abs (y := w)
+      · grind [rename_unused, rename_vars]
+      rw [rename_concat] <;> grind [vars, AlphaEquiv.refl]
     · simp only [rename, hzx, ↓reduceIte]
       obtain ⟨w, hw⟩ := HasFresh.fresh_exists (m.vars ∪ {x, y, z})
-      apply AlphaEquiv.abs (y := w) <;> try grind [rename_unused, rename_vars]
+      apply AlphaEquiv.abs (y := w)
+      · grind [rename_unused, rename_vars]
       apply AlphaEquiv.rename_preserve <;> grind [vars, rename_vars, fv]
   | app m1 m2 ih1 ih2 =>
     apply AlphaEquiv.app
     · apply ih1 <;> grind [vars, fv]
     · apply ih2 <;> grind [vars, fv]
 
+/-- Abstracting over an arbitrary non-free variable results in the same term, modulo α-equivalence. -/
+theorem AlphaEquiv.abs_non_fv [DecidableEq Var] [HasFresh Var] {m1 m2 : Term Var} {x1 x2 : Var} :
+  m1 =α m2 → x1 ∉ m1.fv → x2 ∉ m2.fv → (abs x1 m1) =α (abs x2 m2) := by
+  intro hm hx1 hx2
+  obtain ⟨y, hy⟩ := HasFresh.fresh_exists (m1.vars ∪ m2.vars ∪ {x1, x2})
+  apply AlphaEquiv.abs (y := y)
+  · grind
+  apply AlphaEquiv.trans (n := m1)
+  · grind [rename_non_fv, AlphaEquiv.symm]
+  apply AlphaEquiv.trans (n := m2) <;> grind [rename_non_fv]
+
 /-- Any `Term` can be obtained by filling a `Context` with a variable. This proves that `Context`
 completely captures the syntax of terms. -/
 theorem Context.complete (m : Term Var) :
-    ∃ (c : Context Var) (x : Var), m = (c.fill (Term.var x)) := by
+    ∃ (c : Context Var) (x : Var), m = (c.fill (var x)) := by
   induction m with
   | var x => exists hole, x
   | abs x n ih =>
@@ -261,6 +277,323 @@ theorem Context.complete (m : Term Var) :
     exists Context.appL c₁ n₂, x₁
     rw [ih₁, fill]
 
+/-- The set of variables after filling a context. -/
+theorem Context.fill_vars [DecidableEq Var] {c : Context Var} {m : Term Var} :
+  (c.fill m).vars = c.vars ∪ m.vars := by
+  induction c <;> grind [Context.fill, Context.vars, Term.vars]
+
+/-- α-equivalence is preserved under context filling. -/
+theorem AlphaEquiv.context [DecidableEq Var] [HasFresh Var] {m n : Term Var} {c : Context Var} :
+  m =α n → (c.fill m) =α (c.fill n) := by
+  intro h
+  induction c with
+  | hole => assumption
+  | abs x c ih =>
+    simp only [Context.fill]
+    obtain ⟨y, hy⟩ := HasFresh.fresh_exists (m.vars ∪ n.vars ∪ c.vars ∪ {x})
+    apply AlphaEquiv.abs (y := y) <;> grind [Context.fill_vars, rename_preserve]
+  | appL c m ih =>
+    apply AlphaEquiv.app <;> grind [AlphaEquiv.app, AlphaEquiv.refl, vars]
+  | appR m c ih =>
+    apply AlphaEquiv.app <;> grind [AlphaEquiv.app, AlphaEquiv.refl, vars]
+
+/-- The functional definition of substitution satisfies the relational definition of substitution. -/
+theorem Subst.function_to_relation [DecidableEq Var] [HasFresh Var] {m r : Term Var} {x : Var} :
+  m.Subst x r (m[x := r]) := by
+  refine WellFounded.induction (C := fun m => m.Subst x r (m[x := r])) sizeOfWFRel.wf m ?_
+  simp only; intro m ih
+  cases m with
+  | var y =>
+    by_cases hyx : y = x
+    · subst y
+      simp only [← subst_def, subst.eq_1, ↓reduceIte]
+      apply Subst.varHit
+    · simp [hyx]
+      grind [Subst.varMiss]
+  | abs y m =>
+    by_cases hyx : y = x
+    · subst y
+      simp only [← subst_def, subst.eq_2, ↓reduceIte]
+      apply Subst.absShadow
+    · simp only [← subst_def, subst.eq_2, hyx, ↓reduceIte, Finset.union_insert]
+      by_cases hyr : y ∈ r.fv
+      · simp only [hyr]
+        have hz := fresh_notMem (insert x (insert y (m.vars ∪ r.vars)))
+        set z := fresh (insert x (insert y (m.vars ∪ r.vars)))
+        apply Subst.alpha (m := abs z (m.rename y z)) (r := r) (n := abs z ((m.rename y z)[x := r]))
+        · have h1 : abs z (m.rename y z) = (abs y m).rename y z := by
+            simp [rename]
+          grind [AlphaEquiv.symm, AlphaEquiv.rename_non_fv, vars, fv]
+        · grind [AlphaEquiv.refl]
+        · grind [AlphaEquiv.refl]
+        · apply Subst.absIn
+          · grind [vars, fv, vars_either_fv_or_bv]
+          apply ih
+          grind [rename.eq_sizeOf]
+      · simp only [hyr]
+        apply Subst.absIn
+        · grind [vars, fv, vars_either_fv_or_bv]
+        apply ih
+        grind
+  | app m1 m2 =>
+    simp only [← subst_def, subst.eq_3]
+    apply Subst.app <;> apply ih <;> grind
+
+/-- substituting a non-free variable has no effect. -/
+theorem subst.non_free [DecidableEq Var] [HasFresh Var] {m r : Term Var} {x : Var} :
+  x ∉ m.fv → (m[x := r]) =α m := by
+  refine WellFounded.induction (C := fun m => x ∉ m.fv → (m[x := r]) =α m) sizeOfWFRel.wf m ?_
+  simp only; intro m ih hx
+  cases m with
+  | var y =>
+    have hyx : y ≠ x := by
+      grind [fv]
+    simp only [← subst_def, subst.eq_1, hyx, ↓reduceIte]
+    apply AlphaEquiv.var
+  | abs y m =>
+    by_cases hyx : y = x
+    · subst y
+      simp only [← subst_def, subst.eq_2, ↓reduceIte]
+      apply AlphaEquiv.refl
+    · by_cases hyr : y ∈ r.fv
+      · simp only [← subst_def, subst.eq_2, hyx, ↓reduceIte, hyr, not_true_eq_false,
+          Finset.union_insert, Finset.union_singleton]
+        have hz := fresh_notMem (insert x (insert y (m.vars ∪ r.vars)))
+        set z := fresh (insert x (insert y (m.vars ∪ r.vars)))
+        obtain ⟨w, hw⟩ := HasFresh.fresh_exists (m.vars ∪ r.vars ∪ ((m.rename y z).subst x r).vars
+          ∪ {x, y, z})
+        apply AlphaEquiv.abs (y := w)
+        · grind [vars, rename_unused, rename_vars]
+        apply AlphaEquiv.trans (n := ((m.rename y z).rename z w))
+        · apply AlphaEquiv.rename_preserve
+          · grind [vars, rename_vars, fv]
+          apply ih <;> grind [fv, rename_fv, rename.eq_sizeOf]
+        · grind [rename_concat, AlphaEquiv.refl]
+      · simp only [← subst_def, subst.eq_2, hyx, ↓reduceIte, hyr, not_false_eq_true]
+        apply AlphaEquiv.context (c := Context.abs y Context.hole)
+        apply ih <;> grind [fv]
+  | app m1 m2 =>
+    simp only [← subst_def, subst.eq_3]
+    apply AlphaEquiv.app <;> apply ih <;> grind [fv]
+
+/-- Renaming an abstraction leads to an α-equivalent term. -/
+theorem AlphaEquiv.abs_rename [DecidableEq Var] [HasFresh Var] {m : Term Var} {x y : Var} :
+  y ∉ m.vars ∪ {x} → (abs x m) =α (abs y (m.rename x y)) := by
+  intro hy
+  obtain ⟨z, hz⟩ := HasFresh.fresh_exists (m.vars ∪ {x, y})
+  apply AlphaEquiv.abs (y := z) <;> grind [vars, rename_vars, rename_concat, AlphaEquiv.refl]
+
+lemma AlphaEquiv.subst_abs_fresh_helper [DecidableEq Var] [HasFresh Var]
+  {m r : Term Var} {x y z : Var} :
+  z ∉ m.vars ∪ r.vars ∪ {x, y} →
+  ((abs y m)[x := r]) =α (abs z ((m.rename y z)[x := r]))
+  ∧ (y ∉ r.fv ∪ {x} → (abs y (m[x := r])) =α (abs z ((m.rename y z)[x := r]))) := by
+  refine (WellFounded.induction sizeOfWFRel.wf m
+    (C := fun m => ∀ (r : Term Var) (x y z : Var),
+      z ∉ m.vars ∪ r.vars ∪ {x, y} →
+  ((abs y m)[x := r]) =α (abs z ((m.rename y z)[x := r]))
+  ∧ (y ∉ r.fv ∪ {x} → (abs y (m[x := r])) =α (abs z ((m.rename y z)[x := r])))) ?_) r x y z
+  intro m ih r x y z hz
+  have hright : ∀ (m' : Term Var) (y' : Var), sizeOf m' = sizeOf m → z ∉ m'.vars ∪ r.vars ∪ {x, y'}
+    → y' ∉ r.fv ∪ {x} → (Term.abs y' (m'[x:=r])) =α (Term.abs z ((m'.rename y' z)[x:=r])) := by
+    intro m' y' hm' hz hy'
+    cases m' with
+    | var w =>
+      by_cases hwx : w = x
+      · subst w
+        have hxy' : x ≠ y' := by grind
+        rw [rename]
+        simp only [← subst_def, subst.eq_1, ↓reduceIte, hxy']
+        apply abs_non_fv <;> grind [vars_either_fv_or_bv, AlphaEquiv.refl]
+      · simp only [← subst_def, subst.eq_1, hwx, ↓reduceIte]
+        rw [rename]
+        by_cases hwy' : w = y'
+        · subst w
+          have hzx : z ≠ x := by grind
+          simp only [↓reduceIte, subst.eq_1, hzx]
+          obtain ⟨v, hv⟩ := HasFresh.fresh_exists ({y', z})
+          apply AlphaEquiv.abs (y := v) <;> grind [vars, rename, AlphaEquiv.var]
+        · simp only [hwy', ↓reduceIte, subst.eq_1, hwx]
+          apply abs_non_fv <;> grind [vars_either_fv_or_bv, AlphaEquiv.refl, Term.fv]
+    | app m1 m2 =>
+      obtain ⟨w, hw⟩ := HasFresh.fresh_exists
+        ((m1.app m2)[x := r].vars ∪ (((m1.app m2).rename y' z)[x := r]).vars
+        ∪ m1[x := r].vars ∪ m2[x := r].vars ∪ (m1.rename y' z)[x := r].vars
+        ∪ (m2.rename y' z)[x := r].vars ∪ {y', z})
+      apply AlphaEquiv.abs (y := w)
+      · grind
+      simp only [← subst_def, subst.eq_3, rename]
+      apply AlphaEquiv.app <;> apply AlphaEquiv.abs_elim <;> grind [vars, rename_vars]
+    | abs w m1 =>
+      by_cases hwy' : w = y'
+      · subst w
+        rw [rename]
+        have hy'x : y' ≠ x := by grind
+        have hy'r : y' ∉ r.fv := by grind
+        have hzx : z ≠ x := by grind
+        have hzr : z ∉ r.fv := by grind [vars_either_fv_or_bv]
+        simp only [← subst_def, subst.eq_2, hy'x, ↓reduceIte, hy'r, not_false_eq_true, hzx, hzr]
+        apply abs_non_fv
+        · apply (ih _ _ _ _ _ _ _).right <;> grind [vars]
+        · grind [fv]
+        · grind [fv]
+      · rw [rename]
+        simp only [hwy', ↓reduceIte]
+        by_cases hwx : w = x
+        · subst w
+          simp only [← subst_def, subst, ↓reduceIte]
+          apply AlphaEquiv.trans (n := Term.abs z ((Term.abs x m1).rename y' z))
+          · grind [AlphaEquiv.abs_rename]
+          · grind [rename, AlphaEquiv.refl]
+        · by_cases hwr : w ∈ r.fv
+          · obtain ⟨v, hv⟩ := HasFresh.fresh_exists (m1.vars ∪ r.vars ∪ {x, y', z, w})
+            have hl : (Term.abs y' (((Term.abs w m1)[x := r]))) =α
+                (Term.abs y' (Term.abs v ((m1.rename w v)[x := r]))) := by
+              apply AlphaEquiv.context (c := Context.abs y' Context.hole)
+              apply (ih _ _ _ _ _ _ _).left <;> grind
+            have hr : (Term.abs z (Term.abs v (((m1.rename y' z).rename w v)[x := r])))
+              =α (Term.abs z ((Term.abs w (m1.rename y' z))[x := r])) := by
+              apply AlphaEquiv.context (c := Context.abs z Context.hole)
+              apply AlphaEquiv.symm
+              apply (ih _ _ _ _ _ _ _).left <;> grind [rename_vars, rename.eq_sizeOf]
+            have hmid : (abs y' (abs v ((m1.rename w v)[x := r]))) =α
+                (abs z (abs v (((m1.rename y' z).rename w v)[x := r]))) := by
+              obtain ⟨u, hu⟩ := HasFresh.fresh_exists
+                ((Term.abs v ((m1.rename w v)[x := r])).vars ∪
+                (Term.abs v (((m1.rename y' z).rename w v)[x := r])).vars ∪
+                ((m1.rename w v).rename y' z)[x:=r].vars ∪ {y', z})
+              apply AlphaEquiv.abs (y := u)
+              · grind
+              · have hvy' : v ≠ y' := by grind
+                have hvz : v ≠ z := by grind
+                simp only [rename, hvy', hvz, ↓reduceIte]
+                apply AlphaEquiv.context (c := Context.abs v Context.hole)
+                apply AlphaEquiv.trans (n := (((m1.rename w v).rename y' z)[x := r]).rename z u)
+                · apply AlphaEquiv.abs_elim
+                  · grind  [vars]
+                  · apply (ih _ _ _ _ _ _ _).right <;> grind [vars, rename_vars, rename.eq_sizeOf]
+                · apply rename_preserve
+                  · grind [vars]
+                  · rw [rename_comm] <;> grind [vars, AlphaEquiv.refl]
+            exact AlphaEquiv.trans hl <| AlphaEquiv.trans hmid hr
+          · obtain ⟨v, hv⟩ := HasFresh.fresh_exists
+              (m1[x:=r].vars ∪ (m1.rename y' z)[x:=r].vars ∪ ((Term.abs w m1)[x := r]).vars ∪
+              ((Term.abs w (m1.rename y' z))[x := r]).vars ∪ {y', z})
+            apply AlphaEquiv.abs (y := v)
+            · grind [vars, rename_vars]
+            · have hwz : w ≠ z := by grind [vars]
+              simp only [← subst_def, subst, hwx, ↓reduceIte, hwr, not_false_eq_true, rename, hwy',
+                hwz]
+              apply AlphaEquiv.context (c := Context.abs w Context.hole)
+              apply AlphaEquiv.abs_elim <;> grind [vars]
+  have hleft : ((Term.abs y m)[x:=r]) =α (Term.abs z ((m.rename y z)[x:=r])) := by
+    by_cases hyx : y = x
+    · subst y
+      simp only [← subst_def, subst.eq_2, ↓reduceIte]
+      obtain ⟨w, hw⟩ := HasFresh.fresh_exists (m.vars ∪ r.vars ∪ ((m.rename x z).subst x r).vars ∪
+        {x, z})
+      apply AlphaEquiv.abs (y := w)
+      · grind [vars, rename_unused, rename_vars]
+      · apply AlphaEquiv.trans (n := ((m.rename x z).rename z w))
+        · grind [AlphaEquiv.refl, rename_concat]
+        · apply AlphaEquiv.rename_preserve
+          · grind [rename_vars]
+          · apply AlphaEquiv.symm
+            apply subst.non_free
+            grind [fv, rename_fv, rename.eq_sizeOf]
+    · by_cases hyr : y ∈ r.fv
+      · simp only [← subst_def, subst.eq_2, hyx, ↓reduceIte, hyr, not_true_eq_false,
+          Finset.union_insert, Finset.union_singleton]
+        have hw := fresh_notMem (insert x (insert y (m.vars ∪ r.vars)))
+        set w := fresh (insert x (insert y (m.vars ∪ r.vars)))
+        by_cases hzw' : z = w
+        · subst z
+          apply AlphaEquiv.refl
+        · apply AlphaEquiv.trans (n := (abs z (((m.rename y w).rename w z)[x := r])))
+          · apply hright <;>
+              grind [rename.eq_sizeOf, vars_either_fv_or_bv, rename_vars]
+          · rw [rename_concat] <;> grind [AlphaEquiv.refl]
+      · simp only [← subst_def, subst.eq_2, hyx, ↓reduceIte, hyr, not_false_eq_true]
+        apply hright <;> grind
+  exact ⟨hleft, hright m y (by rfl) (by grind)⟩
+
+/-- Modulo α-equivalence, substituting an abstraction falls back to the fresh variable case only.
+    With this lemma, the three cases in the definition of subst can be reduced to one.
+-/
+theorem AlphaEquiv.subst_abs_fresh [DecidableEq Var] [HasFresh Var]
+  {m r : Term Var} {x y z : Var} :
+  z ∉ m.vars ∪ r.vars ∪ {x, y} →
+  ((abs y m)[x := r]) =α (abs z ((m.rename y z)[x := r])) := by
+  grind [AlphaEquiv.subst_abs_fresh_helper]
+
+/-- Substituting α-equivalent terms produces α-equivalent terms. -/
+theorem subst.preserve_AlphaEquiv [DecidableEq Var] [HasFresh Var]
+  {m m' r r' : Term Var} {x : Var} :
+  m =α m' → r =α r' → (m[x := r]) =α (m'[x := r']) := by
+  refine (WellFounded.induction sizeOfWFRel.wf m
+    (C := fun m => ∀ (m' r r' : Term Var) (x : Var),
+      m =α m' → r =α r' → (m[x := r]) =α (m'[x := r'])) ?_) m' r r' x
+  intro m ih m' r r' x hmm' hrr'
+  have hmm'' := hmm'
+  cases hmm'' with
+  | @var y =>
+    by_cases hyx : y = x
+    · simp only [← subst_def, subst, ↓reduceIte, hyx]
+      assumption
+    · simp only [← subst_def, subst, hyx]
+      apply AlphaEquiv.refl
+  | @abs z y y' m m' hz h1 =>
+    obtain ⟨w, hw⟩ := HasFresh.fresh_exists (m.vars ∪ m'.vars ∪ r.vars ∪ r'.vars ∪ {x, y, y'})
+    have h2 : ((abs y m)[x := r]) =α (abs w ((m.rename y w)[x := r])) := by
+      grind [AlphaEquiv.subst_abs_fresh]
+    have h2' : ((abs y' m')[x := r']) =α
+        (abs w ((m'.rename y' w)[x := r'])) := by
+      grind [AlphaEquiv.subst_abs_fresh]
+    have hbody : (m.rename y w) =α (m'.rename y' w) := by
+      apply AlphaEquiv.abs_elim <;> grind
+    have h3 : (abs w ((m.rename y w)[x := r])) =α (abs w ((m'.rename y' w)[x := r'])) := by
+      apply AlphaEquiv.context (c := Context.abs w Context.hole)
+      apply ih <;> grind [rename.eq_sizeOf]
+    apply AlphaEquiv.trans (n := (abs w ((m.rename y w)[x := r]))) <;> try assumption
+    apply AlphaEquiv.trans (n := (abs w ((m'.rename y' w)[x := r']))) <;> try assumption
+    apply AlphaEquiv.symm
+    assumption
+  | @app m m' n n' hm hn =>
+    simp only [← subst_def, subst]
+    apply AlphaEquiv.app <;> apply ih <;> grind
+
+/-- The relational definition of substitution coincides with the functional definition of
+    substitution, modulo α-equivalence. -/
+theorem Subst.relation_function_iff [DecidableEq Var] [HasFresh Var] {m n r : Term Var} {x : Var} :
+  m.Subst x r n ↔ n =α (m[x := r]) := by
+  constructor
+  · intro h
+    induction h with
+    | @varHit x r =>
+      simp only [← subst_def, subst, ↓reduceIte]
+      apply AlphaEquiv.refl
+    | @varMiss x y r hyx =>
+      simp only [← subst_def, subst, hyx, ↓reduceIte]
+      apply AlphaEquiv.refl
+    | @absShadow x m r =>
+      simp only [← subst_def, subst, ↓reduceIte]
+      apply AlphaEquiv.refl
+    | @absIn x y m r m' hy h ih =>
+      have hyx : y ≠ x := by grind
+      have hyr : y ∉ r.fv := by grind
+      simp only [← subst_def, subst, hyx, ↓reduceIte, hyr, not_false_eq_true]
+      apply AlphaEquiv.context (c := Context.abs y Context.hole)
+      assumption
+    | @app m n x r m' n' h1 h2 ih1 ih2 =>
+      simp only [← subst_def, subst]
+      apply AlphaEquiv.app <;> assumption
+    | @alpha m m' r r' n n' x hm hr hn h ih =>
+      apply AlphaEquiv.trans (n := n)
+      · grind [AlphaEquiv.symm]
+      apply AlphaEquiv.trans (n := m[x := r]) <;> grind [subst.preserve_AlphaEquiv]
+  · intro h
+    apply Subst.alpha (m := m) (r := r) (n := m[x := r]) <;> grind [AlphaEquiv.symm,
+      AlphaEquiv.refl, Subst.function_to_relation]
 
 end LambdaCalculus.Named
 

From e9c56407fe0d6d0fcffae531a86303691cb6f0e7 Mon Sep 17 00:00:00 2001
From: Haoxuan Yin <haoxn.yin@gmail.com>
Date: Wed, 25 Mar 2026 16:02:53 +0000
Subject: [PATCH 6/9] Commutativity of substitution (a.k.a. the substitution
 lemma)

---
 .../Named/Untyped/Properties.lean             | 59 +++++++++++++++++++
 1 file changed, 59 insertions(+)

diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
index ce471e785..2e1d21544 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
@@ -595,6 +595,65 @@ theorem Subst.relation_function_iff [DecidableEq Var] [HasFresh Var] {m n r : Te
     apply Subst.alpha (m := m) (r := r) (n := m[x := r]) <;> grind [AlphaEquiv.symm,
       AlphaEquiv.refl, Subst.function_to_relation]
 
+/-- Commutativity of substitution (a.k.a. the substitution lemma) -/
+theorem subst.commutativity [DecidableEq Var] [HasFresh Var] {m r1 r2 : Term Var} {x y : Var} :
+  x ∉ r2.fv ∪ {y} →
+  ((m[x := r1])[y := r2]) =α ((m[y := r2])[x := (r1[y := r2])]) := by
+  refine WellFounded.induction sizeOfWFRel.wf m
+    (C := fun m => ∀ (r1 r2 : Term Var) (x y : Var),
+      x ∉ r2.fv ∪ {y} →
+      ((m[x := r1])[y := r2]) =α ((m[y := r2])[x := (r1[y := r2])])) ?_ r1 r2 x y
+  intro m ih r1 r2 x y hxy
+  cases m with
+  | var z =>
+    by_cases hzx : z = x
+    · subst z
+      have hxy' : x ≠ y := by grind
+      simp only [← subst_def, subst.eq_1, ↓reduceIte, hxy']
+      apply AlphaEquiv.refl
+    · by_cases hzy : z = y
+      · subst z
+        simp only [← subst_def, subst.eq_1, hzx, ↓reduceIte]
+        apply AlphaEquiv.symm
+        apply subst.non_free
+        grind
+      · simp only [← subst_def, subst.eq_1, hzx, hzy, ↓reduceIte]
+        apply AlphaEquiv.refl
+  | abs z m =>
+    obtain ⟨w, hw⟩ := HasFresh.fresh_exists
+      (m.vars ∪ r1.vars ∪ r2.vars ∪ (r1[y := r2]).vars ∪ {x, y, z})
+    have hl : (((Term.abs z m)[x := r1])[y := r2]) =α
+      (Term.abs w (((m.rename z w)[x := r1])[y := r2])) := by
+      apply AlphaEquiv.trans (n := (((Term.abs w ((m.rename z w)[x := r1]))[y := r2])))
+      · apply subst.preserve_AlphaEquiv
+        · apply AlphaEquiv.subst_abs_fresh
+          grind
+        · apply AlphaEquiv.refl
+      · have hwy : w ≠ y := by grind
+        have hwr2 : w ∉ r2.fv := by grind [vars_either_fv_or_bv]
+        simp only [← subst_def, subst.eq_2, hwy, ↓reduceIte, hwr2, not_false_eq_true]
+        apply AlphaEquiv.refl
+    have hr : (Term.abs w (((m.rename z w)[y := r2])[x := (r1[y := r2])]))
+      =α (((Term.abs z m)[y := r2])[x := (r1[y := r2])]) := by
+      apply AlphaEquiv.symm
+      apply AlphaEquiv.trans (n := ((Term.abs w ((m.rename z w)[y := r2]))[x := (r1[y := r2])]))
+      · apply subst.preserve_AlphaEquiv
+        · apply AlphaEquiv.subst_abs_fresh
+          grind
+        · apply AlphaEquiv.refl
+      · have hwx : w ≠ x := by grind
+        have hwr : w ∉ (r1.subst y r2).fv := by grind [vars_either_fv_or_bv]
+        simp only [← subst_def, subst.eq_2, hwx, ↓reduceIte, hwr, not_false_eq_true]
+        apply AlphaEquiv.refl
+    have hmid : (Term.abs w (((m.rename z w)[x := r1])[y := r2])) =α
+      (Term.abs w (((m.rename z w)[y := r2])[x := (r1[y := r2])])) := by
+      apply AlphaEquiv.context (c := Context.abs w Context.hole)
+      apply ih <;> grind [rename.eq_sizeOf]
+    exact AlphaEquiv.trans hl <| AlphaEquiv.trans hmid hr
+  | app m1 m2 =>
+    simp only [← subst_def, subst.eq_3]
+    apply AlphaEquiv.app <;> apply ih <;> grind
+
 end LambdaCalculus.Named
 
 end Cslib

From 260a20f0534e95b928170c9d1f86cb5a6a9046b9 Mon Sep 17 00:00:00 2001
From: Haoxuan Yin <haoxn.yin@gmail.com>
Date: Wed, 25 Mar 2026 17:11:02 +0000
Subject: [PATCH 7/9] formatting

---
 .../LambdaCalculus/Named/Untyped/Basic.lean   |  61 ++---
 .../Named/Untyped/Properties.lean             | 223 +++++++++---------
 2 files changed, 141 insertions(+), 143 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
index 6ee9b4ce6..a65bae5b2 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
@@ -14,7 +14,7 @@ public import Cslib.Foundations.Syntax.HasSubstitution
 
 /-! # λ-calculus
 
-The untyped λ-calculus.
+The untyped λ-calculus, with a named representation of variables.
 
 ## References
 
@@ -28,9 +28,9 @@ namespace Cslib
 
 universe u
 
-variable {Var : Type u}
+variable {Var : Type u} [DecidableEq Var] [HasFresh Var]
 
-namespace LambdaCalculus.Named
+namespace LambdaCalculus.Named.Untyped
 
 /-- Syntax of terms. -/
 inductive Term (Var : Type u) : Type u where
@@ -39,58 +39,59 @@ inductive Term (Var : Type u) : Type u where
   | app (m n : Term Var)
 deriving DecidableEq
 
+namespace Term
+
 /-- Free variables. -/
-def Term.fv [DecidableEq Var] : Term Var → Finset Var
+def fv : Term Var → Finset Var
   | var x => {x}
   | abs x m => m.fv \ {x}
   | app m n => m.fv ∪ n.fv
 
 /-- Bound variables. -/
-def Term.bv [DecidableEq Var] : Term Var → Finset Var
+def bv : Term Var → Finset Var
   | var _ => ∅
   | abs x m => m.bv ∪ {x}
   | app m n => m.bv ∪ n.bv
 
 /-- Variable names (free and bound) in a term. -/
-def Term.vars [DecidableEq Var] : Term Var → Finset Var
+def vars : Term Var → Finset Var
   | var x => {x}
   | abs x m => m.vars ∪ {x}
   | app m n => m.vars ∪ n.vars
 
 /-- Variable renaming, applying to both free and bound variables.
     `m.rename x y` changes all occurrences of `x` into `y` in `m`. -/
-def Term.rename [DecidableEq Var] (m : Term Var) (x y : Var) : Term Var :=
+def rename (m : Term Var) (x y : Var) : Term Var :=
   match m with
   | var z => var (if z = x then y else z)
   | abs z m' => abs (if z = x then y else z) (m'.rename x y)
   | app n1 n2 => app (n1.rename x y) (n2.rename x y)
 
+omit [HasFresh Var] in
 /-- Renaming preserves size. -/
 @[simp]
-theorem Term.rename.eq_sizeOf {m : Term Var} {x y : Var} [DecidableEq Var] :
-  sizeOf (m.rename x y) = sizeOf m := by
+theorem rename_eq_sizeOf {m : Term Var} {x y : Var} : sizeOf (m.rename x y) = sizeOf m := by
   induction m <;> aesop (add simp [Term.rename])
 
-open Term
-
 /-- α-equivalence. -/
-inductive Term.AlphaEquiv [DecidableEq Var] : Term Var → Term Var → Prop where
-| var {x} : AlphaEquiv (var x) (var x)
-| abs {y x1 x2 m1 m2} : y ∉ m1.vars ∪ m2.vars ∪ {x1, x2} →
-  AlphaEquiv (m1.rename x1 y) (m2.rename x2 y) → AlphaEquiv (abs x1 m1) (abs x2 m2)
-| app {m1 n1 m2 n2} : AlphaEquiv m1 n1 → AlphaEquiv m2 n2 → AlphaEquiv (app m1 m2) (app n1 n2)
+inductive AlphaEquiv : Term Var → Term Var → Prop where
+  | var {x} : AlphaEquiv (var x) (var x)
+  | abs {y x1 x2 m1 m2} : y ∉ m1.vars ∪ m2.vars ∪ {x1, x2} →
+    AlphaEquiv (m1.rename x1 y) (m2.rename x2 y) → AlphaEquiv (abs x1 m1) (abs x2 m2)
+  | app {m1 n1 m2 n2} : AlphaEquiv m1 n1 → AlphaEquiv m2 n2 → AlphaEquiv (app m1 m2) (app n1 n2)
 
 /-- Instance for the notation `m =α n`. -/
-instance instHasAlphaEquivTerm [DecidableEq Var] : HasAlphaEquiv (Term Var) where
-  AlphaEquiv := Term.AlphaEquiv
+instance instHasAlphaEquivTerm : HasAlphaEquiv (Term Var) where
+  AlphaEquiv := AlphaEquiv
 
+omit [HasFresh Var] in
 /-- Allow grind to recognise the notation of α-equivalence. -/
 @[grind ←]
-theorem Term.AlphaEquiv_def [DecidableEq Var] (m n : Term Var) :
-  AlphaEquiv m n ↔ m =α n := by rfl
+theorem AlphaEquiv_def (m n : Term Var) : AlphaEquiv m n ↔ m =α n := by
+  rfl
 
 /-- Capture-avoiding substitution, as an inference system. -/
-inductive Term.Subst [DecidableEq Var] : Term Var → Var → Term Var → Term Var → Prop where
+inductive Subst : Term Var → Var → Term Var → Term Var → Prop where
   | varHit {x r} : (var x).Subst x r r
   | varMiss {x y r} : y ≠ x → (var y).Subst x r (var y)
   | absShadow {x m r} : (abs x m).Subst x r (abs x m)
@@ -101,8 +102,8 @@ inductive Term.Subst [DecidableEq Var] : Term Var → Var → Term Var → Term
 /-- Capture-avoiding substitution. `m.subst x r` replaces the free occurrences of variable `x`
 in `m` with `r`. -/
 @[grind, simp]
-def Term.subst [DecidableEq Var] [HasFresh Var] (m : Term Var) (x : Var) (r : Term Var) :
-  Term Var :=
+def subst (m : Term Var) (x : Var) (r : Term Var) :
+    Term Var :=
   match m with
   | var y => if y = x then r else var y
   | abs y m' =>
@@ -115,17 +116,17 @@ def Term.subst [DecidableEq Var] [HasFresh Var] (m : Term Var) (x : Var) (r : Te
       abs z ((m'.rename y z).subst x r)
   | app m1 m2 => app (m1.subst x r) (m2.subst x r)
 termination_by m
-decreasing_by all_goals grind [rename.eq_sizeOf, abs.sizeOf_spec, app.sizeOf_spec]
+decreasing_by all_goals grind [rename_eq_sizeOf, abs.sizeOf_spec, app.sizeOf_spec]
 
 /-- `Term.subst` is a substitution for λ-terms. Gives access to the notation `m[x := n]`. -/
-instance instHasSubstitutionTerm [DecidableEq Var] [HasFresh Var] :
+instance instHasSubstitutionTerm :
     HasSubstitution (Term Var) Var (Term Var) where
-  subst := Term.subst
+  subst := subst
 
 /-- Allow grind to recognise the notation of substitution. -/
 @[grind ←, simp← ]
-theorem Term.subst_def [DecidableEq Var] (m r : Term Var) (x : Var) [HasFresh Var] :
-  m.subst x r = m[x := r] := by rfl
+theorem subst_def (m r : Term Var) (x : Var) : m.subst x r = m[x := r] := by
+  rfl
 
 /-- Contexts. -/
 inductive Context (Var : Type u) : Type u where
@@ -143,12 +144,12 @@ def Context.fill (c : Context Var) (m : Term Var) : Term Var :=
   | appL c n => Term.app (c.fill m) n
   | appR n c => Term.app n (c.fill m)
 
-def Context.vars [DecidableEq Var] : Context Var → Finset Var
+def Context.vars : Context Var → Finset Var
   | hole => ∅
   | abs x c => c.vars ∪ {x}
   | appL c m => c.vars ∪ m.vars
   | appR m c => m.vars ∪ c.vars
 
-end LambdaCalculus.Named
+end LambdaCalculus.Named.Untyped.Term
 
 end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
index 2e1d21544..b4dcba4ae 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
@@ -14,32 +14,30 @@ namespace Cslib
 
 universe u
 
-variable {Var : Type u}
+variable {Var : Type u} [DecidableEq Var]
 
-namespace LambdaCalculus.Named
-
-open Term
+namespace LambdaCalculus.Named.Untyped.Term
 
 /-- A variable in a term is either free or bound. -/
-theorem vars_either_fv_or_bv [DecidableEq Var] {m : Term Var} :
+theorem vars_either_fv_or_bv {m : Term Var} :
     m.vars = m.fv ∪ m.bv := by
   induction m <;> grind [fv, bv, vars]
 
 /-- Renaming an unused variable has no effect. -/
 @[simp]
-theorem rename_unused [DecidableEq Var] {m : Term Var} {x y : Var} :
+theorem rename_unused {m : Term Var} {x y : Var} :
   x ∉ m.vars → m.rename x y = m := by
   induction m <;> grind [vars, rename]
 
 /-- Renaming a variable to itself has no effect. -/
 @[simp]
-theorem rename_same [DecidableEq Var] {m : Term Var} {x : Var} :
+theorem rename_same {m : Term Var} {x : Var} :
   m.rename x x = m := by
   induction m <;> grind [vars, rename]
 
 /-- Renaming a used variable changes the set of variables. -/
 @[simp]
-theorem rename_vars_used [DecidableEq Var] {m : Term Var} {x y : Var} :
+theorem rename_vars_used {m : Term Var} {x y : Var} :
   x ∈ m.vars → (m.rename x y).vars = m.vars.erase x ∪ {y} := by
   induction m with
   | var z => grind [vars, rename]
@@ -54,42 +52,49 @@ theorem rename_vars_used [DecidableEq Var] {m : Term Var} {x y : Var} :
       grind [vars, rename, rename_unused]
 
 /-- Renaming removes the variable. -/
-theorem rename_remove [DecidableEq Var] {m : Term Var} {x y : Var} :
+theorem rename_remove {m : Term Var} {x y : Var} :
   x ≠ y → x ∉ (m.rename x y).vars := by
   intro hxy
   by_cases hx : x ∈ m.vars <;> grind [rename_vars_used, rename_unused]
 
 /-- The set of variables after renaming. -/
-theorem rename_vars [DecidableEq Var] {m : Term Var} {x y : Var} :
+theorem rename_vars {m : Term Var} {x y : Var} :
   (m.rename x y).vars = m.vars \ {x} ∪ (if x ∈ m.vars then {y} else ∅) := by
   by_cases x ∈ m.vars <;> grind [vars, rename, rename_unused, rename_vars_used]
 
 /-- The set of free variables after renaming. -/
-theorem rename_fv [DecidableEq Var] {m : Term Var} {x y : Var} :
+theorem rename_fv {m : Term Var} {x y : Var} :
   y ∉ m.vars → (m.rename x y).fv = m.fv \ {x} ∪ (if x ∈ m.fv then {y} else ∅) := by
   induction m <;> grind [fv, vars, rename, vars_either_fv_or_bv]
 
 /-- Concatenation of renaming. -/
 @[simp]
-theorem rename_concat [DecidableEq Var] {m : Term Var} {x y z : Var} :
+theorem rename_concat {m : Term Var} {x y z : Var} :
   y ∉ m.vars → (m.rename x y).rename y z = m.rename x z := by
   induction m <;> grind [vars, rename]
 
-/-- Commutativity of renaming. -/
-theorem rename_comm [DecidableEq Var] {m : Term Var} {x y z w : Var} :
+/-- Commutativity of renaming, simpler version. -/
+theorem rename_comm {m : Term Var} {x y z w : Var} :
   x ≠ z → y ∉ m.vars ∪ {x, z} → w ∉ m.vars ∪ {x, z} →
   (m.rename x y).rename z w = (m.rename z w).rename x y := by
   induction m <;> grind [vars, rename]
 
+/-- Commutativity of renaming, more general version. -/
+theorem rename_comm2 {m : Term Var} {x y z w : Var} :
+    y ∉ m.vars ∪ {x, z} → w ∉ m.vars ∪ {x, y, z} →
+    (m.rename x y).rename (if z = x then y else z) w = (m.rename z w).rename x y := by
+  intro hy hw
+  by_cases hzx : z = x
+  · grind [rename_same, rename_unused, rename_concat, rename_vars]
+  · grind [rename_comm]
+
+omit [DecidableEq Var] in
 @[grind ←]
-lemma induction_by_sizeOf {m n : Term Var} :
-  WellFoundedRelation.rel m n ↔
-  sizeOf m < sizeOf n := by
+lemma induction_by_sizeOf {m n : Term Var} : WellFoundedRelation.rel m n ↔ sizeOf m < sizeOf n := by
   rfl
 
 /-- α-equivalent terms have the same size. -/
-theorem AlphaEquiv.eq_sizeOf [DecidableEq Var] {m n : Term Var} :
-  m =α n → sizeOf m = sizeOf n := by
+theorem AlphaEquiv.eq_sizeOf {m n : Term Var} : m =α n → sizeOf m = sizeOf n := by
   intro h
   induction h with
   | @var x => rfl
@@ -99,8 +104,7 @@ theorem AlphaEquiv.eq_sizeOf [DecidableEq Var] {m n : Term Var} :
     grind
 
 /-- α-equivalent terms have the same free variables. -/
-theorem AlphaEquiv.same_fv [DecidableEq Var] {m n : Term Var} :
-  m =α n → m.fv = n.fv := by
+theorem AlphaEquiv.same_fv {m n : Term Var} : m =α n → m.fv = n.fv := by
   intro h
   induction h with
   | @var x => rfl
@@ -113,8 +117,10 @@ theorem AlphaEquiv.same_fv [DecidableEq Var] {m n : Term Var} :
     grind
   | @app m1 n1 m2 n2 h1 h2 ih1 ih2 => grind [Term.fv]
 
+variable [HasFresh Var]
+
 /-- Reflexivity of α-equivalence. -/
-theorem AlphaEquiv.refl [DecidableEq Var] [HasFresh Var] (m : Term Var) : m =α m := by
+theorem AlphaEquiv.refl (m : Term Var) : m =α m := by
   refine WellFounded.induction (C := fun m => m =α m) sizeOfWFRel.wf m ?_
   simp only; intro m ih
   cases m with
@@ -124,13 +130,13 @@ theorem AlphaEquiv.refl [DecidableEq Var] [HasFresh Var] (m : Term Var) : m =α
     apply AlphaEquiv.abs (y := z)
     · grind [rename_vars]
     apply ih
-    grind [rename.eq_sizeOf]
+    grind [rename_eq_sizeOf]
   | app m n =>
     apply AlphaEquiv.app <;> apply ih <;> grind
 
+omit [HasFresh Var] in
 /-- Symmetry of α-equivalence. -/
-theorem AlphaEquiv.symm [DecidableEq Var] [HasFresh Var] {m n : Term Var} :
-  m =α n → n =α m := by
+theorem AlphaEquiv.symm {m n : Term Var} : m =α n → n =α m := by
   intro h
   induction h with
   | @var x => apply AlphaEquiv.var
@@ -139,19 +145,9 @@ theorem AlphaEquiv.symm [DecidableEq Var] [HasFresh Var] {m n : Term Var} :
   | @app m1 n1 m2 n2 hwm1 hwn1 hwm2 hwn2 =>
     apply AlphaEquiv.app <;> assumption
 
-/-- Commutativity of renaming, more general version. -/
-theorem rename_comm2 [DecidableEq Var] {m : Term Var} {x y z w : Var} :
-  y ∉ m.vars ∪ {x, z} → w ∉ m.vars ∪ {x, y, z} →
-  (m.rename x y).rename (if z = x then y else z) w = (m.rename z w).rename x y := by
-  intro hy hw
-  by_cases hzx : z = x
-  · grind [rename_same, rename_unused, rename_concat, rename_vars]
-  · grind [rename_comm]
-
 /-- Renaming α-equivalent terms produces α-equivalent terms. -/
-theorem AlphaEquiv.rename_preserve [DecidableEq Var] [HasFresh Var]
-  (m n : Term Var) (x y : Var) :
-  y ∉ m.vars ∪ n.vars → m =α n → (m.rename x y) =α (n.rename x y) := by
+theorem AlphaEquiv.rename_preserve (m n : Term Var) (x y : Var) :
+    y ∉ m.vars ∪ n.vars → m =α n → (m.rename x y) =α (n.rename x y) := by
   refine (WellFounded.induction sizeOfWFRel.wf m
     (C := fun m => ∀ (n : Term Var) (x y : Var), y ∉ m.vars ∪ n.vars →
       m =α n → (m.rename x y) =α (n.rename x y)) ?_) n x y
@@ -167,10 +163,10 @@ theorem AlphaEquiv.rename_preserve [DecidableEq Var] [HasFresh Var]
     rw [rename_comm2, rename_comm2]
     case neg.abs.a =>
       apply ih
-      · grind [rename.eq_sizeOf]
+      · grind [rename_eq_sizeOf]
       · grind [vars, rename_vars]
       · have hxzw : ((m1.rename x1 z).rename z w) =α ((m2.rename x2 z).rename z w) := by
-          apply ih <;> grind [vars, rename_vars, rename.eq_sizeOf]
+          apply ih <;> grind [vars, rename_vars, rename_eq_sizeOf]
         grind [rename_concat]
     all_goals grind [vars]
   | @app m1 n1 m2 n2 hm hn =>
@@ -181,9 +177,9 @@ theorem AlphaEquiv.rename_preserve [DecidableEq Var] [HasFresh Var]
     then their bodies can be renamed to ``any'' fresh variable y and remain α-equivalent.
     This is sometimes easier to use than using by_cases on the equivalence,
     which can only produce the claim for ``some'' fresh y. -/
-theorem AlphaEquiv.abs_elim [DecidableEq Var] [HasFresh Var] {m1 m2 : Term Var} {x1 x2 y : Var} :
-  y ∉ m1.vars ∪ m2.vars ∪ {x1, x2} → (abs x1 m1) =α (abs x2 m2) →
-  (m1.rename x1 y) =α (m2.rename x2 y) := by
+theorem AlphaEquiv.abs_elim {m1 m2 : Term Var} {x1 x2 y : Var} :
+    y ∉ m1.vars ∪ m2.vars ∪ {x1, x2} → (Term.abs x1 m1) =α (Term.abs x2 m2) →
+    (m1.rename x1 y) =α (m2.rename x2 y) := by
   intro hy h
   cases h with
   | @abs z _ _ _ _ hz h1 =>
@@ -194,8 +190,8 @@ theorem AlphaEquiv.abs_elim [DecidableEq Var] [HasFresh Var] {m1 m2 : Term Var}
       grind [rename_concat, rename_vars]
 
 /-- Transitivity of α-equivalence. -/
-theorem AlphaEquiv.trans [DecidableEq Var] [HasFresh Var] {m n p : Term Var} :
-  m =α n → n =α p → m =α p := by
+theorem AlphaEquiv.trans {m n p : Term Var} :
+    m =α n → n =α p → m =α p := by
   refine (WellFounded.induction sizeOfWFRel.wf m
     (C := fun m => ∀ (n p : Term Var),
       m =α n → n =α p → m =α p) ?_) n p
@@ -215,7 +211,7 @@ theorem AlphaEquiv.trans [DecidableEq Var] [HasFresh Var] {m n p : Term Var} :
         apply AlphaEquiv.abs (y := w)
         · grind [vars, rename_unused, rename_vars, rename_concat]
         apply ih _ ?_ (m2.rename x2 w) <;>
-        grind [AlphaEquiv.abs_elim, vars, rename_vars, rename.eq_sizeOf]
+        grind [AlphaEquiv.abs_elim, vars, rename_vars, rename_eq_sizeOf]
   | app m1 m2 =>
     cases hmn with
     | @app m1 n1 m2 n2 hmn1 hmn2 =>
@@ -226,8 +222,9 @@ theorem AlphaEquiv.trans [DecidableEq Var] [HasFresh Var] {m n p : Term Var} :
         · apply ih _ ?_ n2 <;> grind [vars, rename_vars]
 
 /-- Renaming a non-free variable result in an α-equivalent term -/
-theorem AlphaEquiv.rename_non_fv [DecidableEq Var] [HasFresh Var] (m : Term Var) (x y : Var)
-  (hxm : x ∉ m.fv) (hym : y ∉ m.vars) : m =α (m.rename x y) := by
+theorem AlphaEquiv.rename_non_fv {m : Term Var} {x y : Var} :
+    x ∉ m.fv → y ∉ m.vars → m =α (m.rename x y) := by
+  intro hx hy
   induction m with
   | var z =>
     have hzx : z ≠ x := by
@@ -251,9 +248,10 @@ theorem AlphaEquiv.rename_non_fv [DecidableEq Var] [HasFresh Var] (m : Term Var)
     · apply ih1 <;> grind [vars, fv]
     · apply ih2 <;> grind [vars, fv]
 
-/-- Abstracting over an arbitrary non-free variable results in the same term, modulo α-equivalence. -/
-theorem AlphaEquiv.abs_non_fv [DecidableEq Var] [HasFresh Var] {m1 m2 : Term Var} {x1 x2 : Var} :
-  m1 =α m2 → x1 ∉ m1.fv → x2 ∉ m2.fv → (abs x1 m1) =α (abs x2 m2) := by
+/-- Abstracting over an arbitrary non-free variable results in the same term,
+    modulo α-equivalence. -/
+theorem AlphaEquiv.abs_non_fv {m1 m2 : Term Var} {x1 x2 : Var} :
+    m1 =α m2 → x1 ∉ m1.fv → x2 ∉ m2.fv → (Term.abs x1 m1) =α (Term.abs x2 m2) := by
   intro hm hx1 hx2
   obtain ⟨y, hy⟩ := HasFresh.fresh_exists (m1.vars ∪ m2.vars ∪ {x1, x2})
   apply AlphaEquiv.abs (y := y)
@@ -262,6 +260,14 @@ theorem AlphaEquiv.abs_non_fv [DecidableEq Var] [HasFresh Var] {m1 m2 : Term Var
   · grind [rename_non_fv, AlphaEquiv.symm]
   apply AlphaEquiv.trans (n := m2) <;> grind [rename_non_fv]
 
+/-- Renaming an abstraction leads to an α-equivalent term. -/
+theorem AlphaEquiv.abs_rename {m : Term Var} {x y : Var} :
+    y ∉ m.vars ∪ {x} → (Term.abs x m) =α (Term.abs y (m.rename x y)) := by
+  intro hy
+  obtain ⟨z, hz⟩ := HasFresh.fresh_exists (m.vars ∪ {x, y})
+  apply AlphaEquiv.abs (y := z) <;> grind [vars, rename_vars, rename_concat, AlphaEquiv.refl]
+
+omit [DecidableEq Var] [HasFresh Var] in
 /-- Any `Term` can be obtained by filling a `Context` with a variable. This proves that `Context`
 completely captures the syntax of terms. -/
 theorem Context.complete (m : Term Var) :
@@ -277,14 +283,15 @@ theorem Context.complete (m : Term Var) :
     exists Context.appL c₁ n₂, x₁
     rw [ih₁, fill]
 
+omit [HasFresh Var] in
 /-- The set of variables after filling a context. -/
-theorem Context.fill_vars [DecidableEq Var] {c : Context Var} {m : Term Var} :
-  (c.fill m).vars = c.vars ∪ m.vars := by
+theorem Context.fill_vars {c : Context Var} {m : Term Var} :
+    (c.fill m).vars = c.vars ∪ m.vars := by
   induction c <;> grind [Context.fill, Context.vars, Term.vars]
 
 /-- α-equivalence is preserved under context filling. -/
-theorem AlphaEquiv.context [DecidableEq Var] [HasFresh Var] {m n : Term Var} {c : Context Var} :
-  m =α n → (c.fill m) =α (c.fill n) := by
+theorem AlphaEquiv.context {m n : Term Var} {c : Context Var} :
+    m =α n → (c.fill m) =α (c.fill n) := by
   intro h
   induction c with
   | hole => assumption
@@ -297,9 +304,10 @@ theorem AlphaEquiv.context [DecidableEq Var] [HasFresh Var] {m n : Term Var} {c
   | appR m c ih =>
     apply AlphaEquiv.app <;> grind [AlphaEquiv.app, AlphaEquiv.refl, vars]
 
-/-- The functional definition of substitution satisfies the relational definition of substitution. -/
-theorem Subst.function_to_relation [DecidableEq Var] [HasFresh Var] {m r : Term Var} {x : Var} :
-  m.Subst x r (m[x := r]) := by
+/-- The functional definition of substitution satisfies the relational definition of substitution.
+-/
+theorem Subst.function_to_relation {m r : Term Var} {x : Var} :
+    m.Subst x r (m[x := r]) := by
   refine WellFounded.induction (C := fun m => m.Subst x r (m[x := r])) sizeOfWFRel.wf m ?_
   simp only; intro m ih
   cases m with
@@ -329,7 +337,7 @@ theorem Subst.function_to_relation [DecidableEq Var] [HasFresh Var] {m r : Term
         · apply Subst.absIn
           · grind [vars, fv, vars_either_fv_or_bv]
           apply ih
-          grind [rename.eq_sizeOf]
+          grind [rename_eq_sizeOf]
       · simp only [hyr]
         apply Subst.absIn
         · grind [vars, fv, vars_either_fv_or_bv]
@@ -339,9 +347,9 @@ theorem Subst.function_to_relation [DecidableEq Var] [HasFresh Var] {m r : Term
     simp only [← subst_def, subst.eq_3]
     apply Subst.app <;> apply ih <;> grind
 
-/-- substituting a non-free variable has no effect. -/
-theorem subst.non_free [DecidableEq Var] [HasFresh Var] {m r : Term Var} {x : Var} :
-  x ∉ m.fv → (m[x := r]) =α m := by
+/-- Substituting a non-free variable has no effect. -/
+theorem subst.non_free {m r : Term Var} {x : Var} :
+    x ∉ m.fv → (m[x := r]) =α m := by
   refine WellFounded.induction (C := fun m => x ∉ m.fv → (m[x := r]) =α m) sizeOfWFRel.wf m ?_
   simp only; intro m ih hx
   cases m with
@@ -367,7 +375,7 @@ theorem subst.non_free [DecidableEq Var] [HasFresh Var] {m r : Term Var} {x : Va
         apply AlphaEquiv.trans (n := ((m.rename y z).rename z w))
         · apply AlphaEquiv.rename_preserve
           · grind [vars, rename_vars, fv]
-          apply ih <;> grind [fv, rename_fv, rename.eq_sizeOf]
+          apply ih <;> grind [fv, rename_fv, rename_eq_sizeOf]
         · grind [rename_concat, AlphaEquiv.refl]
       · simp only [← subst_def, subst.eq_2, hyx, ↓reduceIte, hyr, not_false_eq_true]
         apply AlphaEquiv.context (c := Context.abs y Context.hole)
@@ -376,23 +384,15 @@ theorem subst.non_free [DecidableEq Var] [HasFresh Var] {m r : Term Var} {x : Va
     simp only [← subst_def, subst.eq_3]
     apply AlphaEquiv.app <;> apply ih <;> grind [fv]
 
-/-- Renaming an abstraction leads to an α-equivalent term. -/
-theorem AlphaEquiv.abs_rename [DecidableEq Var] [HasFresh Var] {m : Term Var} {x y : Var} :
-  y ∉ m.vars ∪ {x} → (abs x m) =α (abs y (m.rename x y)) := by
-  intro hy
-  obtain ⟨z, hz⟩ := HasFresh.fresh_exists (m.vars ∪ {x, y})
-  apply AlphaEquiv.abs (y := z) <;> grind [vars, rename_vars, rename_concat, AlphaEquiv.refl]
-
-lemma AlphaEquiv.subst_abs_fresh_helper [DecidableEq Var] [HasFresh Var]
-  {m r : Term Var} {x y z : Var} :
-  z ∉ m.vars ∪ r.vars ∪ {x, y} →
-  ((abs y m)[x := r]) =α (abs z ((m.rename y z)[x := r]))
-  ∧ (y ∉ r.fv ∪ {x} → (abs y (m[x := r])) =α (abs z ((m.rename y z)[x := r]))) := by
+lemma subst.abs_fresh_helper {m r : Term Var} {x y z : Var} :
+    z ∉ m.vars ∪ r.vars ∪ {x, y} →
+    ((Term.abs y m)[x := r]) =α (Term.abs z ((m.rename y z)[x := r]))
+    ∧ (y ∉ r.fv ∪ {x} → (Term.abs y (m[x := r])) =α (Term.abs z ((m.rename y z)[x := r]))) := by
   refine (WellFounded.induction sizeOfWFRel.wf m
     (C := fun m => ∀ (r : Term Var) (x y z : Var),
       z ∉ m.vars ∪ r.vars ∪ {x, y} →
-  ((abs y m)[x := r]) =α (abs z ((m.rename y z)[x := r]))
-  ∧ (y ∉ r.fv ∪ {x} → (abs y (m[x := r])) =α (abs z ((m.rename y z)[x := r])))) ?_) r x y z
+  ((Term.abs y m)[x := r]) =α (Term.abs z ((m.rename y z)[x := r]))
+  ∧ (y ∉ r.fv ∪ {x} → (Term.abs y (m[x := r])) =α (Term.abs z ((m.rename y z)[x := r])))) ?_) r x y z
   intro m ih r x y z hz
   have hright : ∀ (m' : Term Var) (y' : Var), sizeOf m' = sizeOf m → z ∉ m'.vars ∪ r.vars ∪ {x, y'}
     → y' ∉ r.fv ∪ {x} → (Term.abs y' (m'[x:=r])) =α (Term.abs z ((m'.rename y' z)[x:=r])) := by
@@ -404,7 +404,7 @@ lemma AlphaEquiv.subst_abs_fresh_helper [DecidableEq Var] [HasFresh Var]
         have hxy' : x ≠ y' := by grind
         rw [rename]
         simp only [← subst_def, subst.eq_1, ↓reduceIte, hxy']
-        apply abs_non_fv <;> grind [vars_either_fv_or_bv, AlphaEquiv.refl]
+        apply AlphaEquiv.abs_non_fv <;> grind [vars_either_fv_or_bv, AlphaEquiv.refl]
       · simp only [← subst_def, subst.eq_1, hwx, ↓reduceIte]
         rw [rename]
         by_cases hwy' : w = y'
@@ -414,7 +414,7 @@ lemma AlphaEquiv.subst_abs_fresh_helper [DecidableEq Var] [HasFresh Var]
           obtain ⟨v, hv⟩ := HasFresh.fresh_exists ({y', z})
           apply AlphaEquiv.abs (y := v) <;> grind [vars, rename, AlphaEquiv.var]
         · simp only [hwy', ↓reduceIte, subst.eq_1, hwx]
-          apply abs_non_fv <;> grind [vars_either_fv_or_bv, AlphaEquiv.refl, Term.fv]
+          apply AlphaEquiv.abs_non_fv <;> grind [vars_either_fv_or_bv, AlphaEquiv.refl, Term.fv]
     | app m1 m2 =>
       obtain ⟨w, hw⟩ := HasFresh.fresh_exists
         ((m1.app m2)[x := r].vars ∪ (((m1.app m2).rename y' z)[x := r]).vars
@@ -433,7 +433,7 @@ lemma AlphaEquiv.subst_abs_fresh_helper [DecidableEq Var] [HasFresh Var]
         have hzx : z ≠ x := by grind
         have hzr : z ∉ r.fv := by grind [vars_either_fv_or_bv]
         simp only [← subst_def, subst.eq_2, hy'x, ↓reduceIte, hy'r, not_false_eq_true, hzx, hzr]
-        apply abs_non_fv
+        apply AlphaEquiv.abs_non_fv
         · apply (ih _ _ _ _ _ _ _).right <;> grind [vars]
         · grind [fv]
         · grind [fv]
@@ -455,9 +455,9 @@ lemma AlphaEquiv.subst_abs_fresh_helper [DecidableEq Var] [HasFresh Var]
               =α (Term.abs z ((Term.abs w (m1.rename y' z))[x := r])) := by
               apply AlphaEquiv.context (c := Context.abs z Context.hole)
               apply AlphaEquiv.symm
-              apply (ih _ _ _ _ _ _ _).left <;> grind [rename_vars, rename.eq_sizeOf]
-            have hmid : (abs y' (abs v ((m1.rename w v)[x := r]))) =α
-                (abs z (abs v (((m1.rename y' z).rename w v)[x := r]))) := by
+              apply (ih _ _ _ _ _ _ _).left <;> grind [rename_vars, rename_eq_sizeOf]
+            have hmid : (Term.abs y' (Term.abs v ((m1.rename w v)[x := r]))) =α
+                (Term.abs z (Term.abs v (((m1.rename y' z).rename w v)[x := r]))) := by
               obtain ⟨u, hu⟩ := HasFresh.fresh_exists
                 ((Term.abs v ((m1.rename w v)[x := r])).vars ∪
                 (Term.abs v (((m1.rename y' z).rename w v)[x := r])).vars ∪
@@ -471,8 +471,8 @@ lemma AlphaEquiv.subst_abs_fresh_helper [DecidableEq Var] [HasFresh Var]
                 apply AlphaEquiv.trans (n := (((m1.rename w v).rename y' z)[x := r]).rename z u)
                 · apply AlphaEquiv.abs_elim
                   · grind  [vars]
-                  · apply (ih _ _ _ _ _ _ _).right <;> grind [vars, rename_vars, rename.eq_sizeOf]
-                · apply rename_preserve
+                  · apply (ih _ _ _ _ _ _ _).right <;> grind [vars, rename_vars, rename_eq_sizeOf]
+                · apply AlphaEquiv.rename_preserve
                   · grind [vars]
                   · rw [rename_comm] <;> grind [vars, AlphaEquiv.refl]
             exact AlphaEquiv.trans hl <| AlphaEquiv.trans hmid hr
@@ -500,7 +500,7 @@ lemma AlphaEquiv.subst_abs_fresh_helper [DecidableEq Var] [HasFresh Var]
           · grind [rename_vars]
           · apply AlphaEquiv.symm
             apply subst.non_free
-            grind [fv, rename_fv, rename.eq_sizeOf]
+            grind [fv, rename_fv, rename_eq_sizeOf]
     · by_cases hyr : y ∈ r.fv
       · simp only [← subst_def, subst.eq_2, hyx, ↓reduceIte, hyr, not_true_eq_false,
           Finset.union_insert, Finset.union_singleton]
@@ -509,9 +509,9 @@ lemma AlphaEquiv.subst_abs_fresh_helper [DecidableEq Var] [HasFresh Var]
         by_cases hzw' : z = w
         · subst z
           apply AlphaEquiv.refl
-        · apply AlphaEquiv.trans (n := (abs z (((m.rename y w).rename w z)[x := r])))
+        · apply AlphaEquiv.trans (n := (Term.abs z (((m.rename y w).rename w z)[x := r])))
           · apply hright <;>
-              grind [rename.eq_sizeOf, vars_either_fv_or_bv, rename_vars]
+              grind [rename_eq_sizeOf, vars_either_fv_or_bv, rename_vars]
           · rw [rename_concat] <;> grind [AlphaEquiv.refl]
       · simp only [← subst_def, subst.eq_2, hyx, ↓reduceIte, hyr, not_false_eq_true]
         apply hright <;> grind
@@ -520,16 +520,14 @@ lemma AlphaEquiv.subst_abs_fresh_helper [DecidableEq Var] [HasFresh Var]
 /-- Modulo α-equivalence, substituting an abstraction falls back to the fresh variable case only.
     With this lemma, the three cases in the definition of subst can be reduced to one.
 -/
-theorem AlphaEquiv.subst_abs_fresh [DecidableEq Var] [HasFresh Var]
-  {m r : Term Var} {x y z : Var} :
-  z ∉ m.vars ∪ r.vars ∪ {x, y} →
-  ((abs y m)[x := r]) =α (abs z ((m.rename y z)[x := r])) := by
-  grind [AlphaEquiv.subst_abs_fresh_helper]
+theorem subst.abs_fresh {m r : Term Var} {x y z : Var} :
+    z ∉ m.vars ∪ r.vars ∪ {x, y} →
+    ((Term.abs y m)[x := r]) =α (Term.abs z ((m.rename y z)[x := r])) := by
+  grind [subst.abs_fresh_helper]
 
 /-- Substituting α-equivalent terms produces α-equivalent terms. -/
-theorem subst.preserve_AlphaEquiv [DecidableEq Var] [HasFresh Var]
-  {m m' r r' : Term Var} {x : Var} :
-  m =α m' → r =α r' → (m[x := r]) =α (m'[x := r']) := by
+theorem subst.preserve_AlphaEquiv {m m' r r' : Term Var} {x : Var} :
+    m =α m' → r =α r' → (m[x := r]) =α (m'[x := r']) := by
   refine (WellFounded.induction sizeOfWFRel.wf m
     (C := fun m => ∀ (m' r r' : Term Var) (x : Var),
       m =α m' → r =α r' → (m[x := r]) =α (m'[x := r'])) ?_) m' r r' x
@@ -544,18 +542,18 @@ theorem subst.preserve_AlphaEquiv [DecidableEq Var] [HasFresh Var]
       apply AlphaEquiv.refl
   | @abs z y y' m m' hz h1 =>
     obtain ⟨w, hw⟩ := HasFresh.fresh_exists (m.vars ∪ m'.vars ∪ r.vars ∪ r'.vars ∪ {x, y, y'})
-    have h2 : ((abs y m)[x := r]) =α (abs w ((m.rename y w)[x := r])) := by
-      grind [AlphaEquiv.subst_abs_fresh]
-    have h2' : ((abs y' m')[x := r']) =α
-        (abs w ((m'.rename y' w)[x := r'])) := by
-      grind [AlphaEquiv.subst_abs_fresh]
+    have h2 : ((Term.abs y m)[x := r]) =α (Term.abs w ((m.rename y w)[x := r])) := by
+      grind [subst.abs_fresh]
+    have h2' : ((Term.abs y' m')[x := r']) =α
+        (Term.abs w ((m'.rename y' w)[x := r'])) := by
+      grind [subst.abs_fresh]
     have hbody : (m.rename y w) =α (m'.rename y' w) := by
       apply AlphaEquiv.abs_elim <;> grind
-    have h3 : (abs w ((m.rename y w)[x := r])) =α (abs w ((m'.rename y' w)[x := r'])) := by
+    have h3 : (Term.abs w ((m.rename y w)[x := r])) =α (Term.abs w ((m'.rename y' w)[x := r'])) := by
       apply AlphaEquiv.context (c := Context.abs w Context.hole)
-      apply ih <;> grind [rename.eq_sizeOf]
-    apply AlphaEquiv.trans (n := (abs w ((m.rename y w)[x := r]))) <;> try assumption
-    apply AlphaEquiv.trans (n := (abs w ((m'.rename y' w)[x := r']))) <;> try assumption
+      apply ih <;> grind [rename_eq_sizeOf]
+    apply AlphaEquiv.trans (n := (Term.abs w ((m.rename y w)[x := r]))) <;> try assumption
+    apply AlphaEquiv.trans (n := (Term.abs w ((m'.rename y' w)[x := r']))) <;> try assumption
     apply AlphaEquiv.symm
     assumption
   | @app m m' n n' hm hn =>
@@ -564,8 +562,8 @@ theorem subst.preserve_AlphaEquiv [DecidableEq Var] [HasFresh Var]
 
 /-- The relational definition of substitution coincides with the functional definition of
     substitution, modulo α-equivalence. -/
-theorem Subst.relation_function_iff [DecidableEq Var] [HasFresh Var] {m n r : Term Var} {x : Var} :
-  m.Subst x r n ↔ n =α (m[x := r]) := by
+theorem Subst.relation_iff_function {m n r : Term Var} {x : Var} :
+    m.Subst x r n ↔ n =α (m[x := r]) := by
   constructor
   · intro h
     induction h with
@@ -596,9 +594,8 @@ theorem Subst.relation_function_iff [DecidableEq Var] [HasFresh Var] {m n r : Te
       AlphaEquiv.refl, Subst.function_to_relation]
 
 /-- Commutativity of substitution (a.k.a. the substitution lemma) -/
-theorem subst.commutativity [DecidableEq Var] [HasFresh Var] {m r1 r2 : Term Var} {x y : Var} :
-  x ∉ r2.fv ∪ {y} →
-  ((m[x := r1])[y := r2]) =α ((m[y := r2])[x := (r1[y := r2])]) := by
+theorem subst.commutativity {m r1 r2 : Term Var} {x y : Var} :
+    x ∉ r2.fv ∪ {y} → ((m[x := r1])[y := r2]) =α ((m[y := r2])[x := (r1[y := r2])]) := by
   refine WellFounded.induction sizeOfWFRel.wf m
     (C := fun m => ∀ (r1 r2 : Term Var) (x y : Var),
       x ∉ r2.fv ∪ {y} →
@@ -626,7 +623,7 @@ theorem subst.commutativity [DecidableEq Var] [HasFresh Var] {m r1 r2 : Term Var
       (Term.abs w (((m.rename z w)[x := r1])[y := r2])) := by
       apply AlphaEquiv.trans (n := (((Term.abs w ((m.rename z w)[x := r1]))[y := r2])))
       · apply subst.preserve_AlphaEquiv
-        · apply AlphaEquiv.subst_abs_fresh
+        · apply subst.abs_fresh
           grind
         · apply AlphaEquiv.refl
       · have hwy : w ≠ y := by grind
@@ -638,7 +635,7 @@ theorem subst.commutativity [DecidableEq Var] [HasFresh Var] {m r1 r2 : Term Var
       apply AlphaEquiv.symm
       apply AlphaEquiv.trans (n := ((Term.abs w ((m.rename z w)[y := r2]))[x := (r1[y := r2])]))
       · apply subst.preserve_AlphaEquiv
-        · apply AlphaEquiv.subst_abs_fresh
+        · apply subst.abs_fresh
           grind
         · apply AlphaEquiv.refl
       · have hwx : w ≠ x := by grind
@@ -648,12 +645,12 @@ theorem subst.commutativity [DecidableEq Var] [HasFresh Var] {m r1 r2 : Term Var
     have hmid : (Term.abs w (((m.rename z w)[x := r1])[y := r2])) =α
       (Term.abs w (((m.rename z w)[y := r2])[x := (r1[y := r2])])) := by
       apply AlphaEquiv.context (c := Context.abs w Context.hole)
-      apply ih <;> grind [rename.eq_sizeOf]
+      apply ih <;> grind [rename_eq_sizeOf]
     exact AlphaEquiv.trans hl <| AlphaEquiv.trans hmid hr
   | app m1 m2 =>
     simp only [← subst_def, subst.eq_3]
     apply AlphaEquiv.app <;> apply ih <;> grind
 
-end LambdaCalculus.Named
+end LambdaCalculus.Named.Untyped.Term
 
 end Cslib

From f830131fee56e938a6e284935eb2c04794160210 Mon Sep 17 00:00:00 2001
From: Haoxuan Yin <haoxn.yin@gmail.com>
Date: Wed, 25 Mar 2026 17:51:20 +0000
Subject: [PATCH 8/9] fix copilot suggestions

---
 Cslib.lean                                         |  1 +
 .../LambdaCalculus/Named/Untyped/Basic.lean        |  2 +-
 .../LambdaCalculus/Named/Untyped/Properties.lean   | 14 ++++++++------
 3 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/Cslib.lean b/Cslib.lean
index a9d5ffc3e..d4938b80c 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -93,6 +93,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaCon
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.Properties
 public import Cslib.Logics.HML.Basic
 public import Cslib.Logics.LinearLogic.CLL.Basic
 public import Cslib.Logics.LinearLogic.CLL.CutElimination
diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
index a65bae5b2..d43b04072 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
@@ -124,7 +124,7 @@ instance instHasSubstitutionTerm :
   subst := subst
 
 /-- Allow grind to recognise the notation of substitution. -/
-@[grind ←, simp← ]
+@[grind ←]
 theorem subst_def (m r : Term Var) (x : Var) : m.subst x r = m[x := r] := by
   rfl
 
diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
index b4dcba4ae..1589c526e 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
@@ -221,7 +221,7 @@ theorem AlphaEquiv.trans {m n p : Term Var} :
         · apply ih _ ?_ n1 <;> grind [vars, rename_vars]
         · apply ih _ ?_ n2 <;> grind [vars, rename_vars]
 
-/-- Renaming a non-free variable result in an α-equivalent term -/
+/-- Renaming a non-free variable results in an α-equivalent term -/
 theorem AlphaEquiv.rename_non_fv {m : Term Var} {x y : Var} :
     x ∉ m.fv → y ∉ m.vars → m =α (m.rename x y) := by
   intro hx hy
@@ -316,7 +316,7 @@ theorem Subst.function_to_relation {m r : Term Var} {x : Var} :
     · subst y
       simp only [← subst_def, subst.eq_1, ↓reduceIte]
       apply Subst.varHit
-    · simp [hyx]
+    · simp [hyx, ← subst_def]
       grind [Subst.varMiss]
   | abs y m =>
     by_cases hyx : y = x
@@ -390,9 +390,10 @@ lemma subst.abs_fresh_helper {m r : Term Var} {x y z : Var} :
     ∧ (y ∉ r.fv ∪ {x} → (Term.abs y (m[x := r])) =α (Term.abs z ((m.rename y z)[x := r]))) := by
   refine (WellFounded.induction sizeOfWFRel.wf m
     (C := fun m => ∀ (r : Term Var) (x y z : Var),
-      z ∉ m.vars ∪ r.vars ∪ {x, y} →
-  ((Term.abs y m)[x := r]) =α (Term.abs z ((m.rename y z)[x := r]))
-  ∧ (y ∉ r.fv ∪ {x} → (Term.abs y (m[x := r])) =α (Term.abs z ((m.rename y z)[x := r])))) ?_) r x y z
+    z ∉ m.vars ∪ r.vars ∪ {x, y} →
+    ((Term.abs y m)[x := r]) =α (Term.abs z ((m.rename y z)[x := r]))
+    ∧ (y ∉ r.fv ∪ {x} → (Term.abs y (m[x := r])) =α (Term.abs z ((m.rename y z)[x := r])))) ?_)
+    r x y z
   intro m ih r x y z hz
   have hright : ∀ (m' : Term Var) (y' : Var), sizeOf m' = sizeOf m → z ∉ m'.vars ∪ r.vars ∪ {x, y'}
     → y' ∉ r.fv ∪ {x} → (Term.abs y' (m'[x:=r])) =α (Term.abs z ((m'.rename y' z)[x:=r])) := by
@@ -549,7 +550,8 @@ theorem subst.preserve_AlphaEquiv {m m' r r' : Term Var} {x : Var} :
       grind [subst.abs_fresh]
     have hbody : (m.rename y w) =α (m'.rename y' w) := by
       apply AlphaEquiv.abs_elim <;> grind
-    have h3 : (Term.abs w ((m.rename y w)[x := r])) =α (Term.abs w ((m'.rename y' w)[x := r'])) := by
+    have h3 :
+        (Term.abs w ((m.rename y w)[x := r])) =α (Term.abs w ((m'.rename y' w)[x := r'])) := by
       apply AlphaEquiv.context (c := Context.abs w Context.hole)
       apply ih <;> grind [rename_eq_sizeOf]
     apply AlphaEquiv.trans (n := (Term.abs w ((m.rename y w)[x := r]))) <;> try assumption

From aaedda90bde7940e8d74de76b016c7d8b0743219 Mon Sep 17 00:00:00 2001
From: Haoxuan Yin <haoxn.yin@gmail.com>
Date: Thu, 26 Mar 2026 09:21:51 +0000
Subject: [PATCH 9/9] fix test fail

---
 CslibTests/LambdaCalculus.lean | 51 +++++++++++++++++++---------------
 1 file changed, 29 insertions(+), 22 deletions(-)

diff --git a/CslibTests/LambdaCalculus.lean b/CslibTests/LambdaCalculus.lean
index 1a331ea58..b0743e63e 100644
--- a/CslibTests/LambdaCalculus.lean
+++ b/CslibTests/LambdaCalculus.lean
@@ -1,42 +1,49 @@
 /-
 Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fabrizio Montesi
+Authors: Fabrizio Montesi, Haoxuan Yin
 -/
 
 import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
-
-
+import CsLib.Languages.LambdaCalculus.Named.Untyped.Properties
 
 namespace CslibTests
 
-open Cslib LambdaCalculus.Named LambdaCalculus.Named.Term
-
-abbrev NatTerm := Term ℕ
-
-def lambdaId := abs 0 (var 0)
-
-example : (abs 0 (var 0)) =α (abs 1 (var 1)) := by
-  constructor
-  simp [Term.fv]
-
-example : (abs 1 (var 0)).subst 0 (app (var 1) (var 2)) = (abs 3 (app (var 1) (var 2))) := by
-  simp +instances [subst, fv, bv, vars, rename, instHasFreshNat, HasFresh.ofSucc]
+open Cslib Cslib.LambdaCalculus.Named.Untyped.Term
 
 def x := 0
 def y := 1
 def z := 2
 def w := 3
 
-attribute [simp] x y z w
+def lambdaId := abs x (var x)
 
-local instance coeNatTerm : Coe ℕ (Term ℕ) := ⟨Term.var⟩
+example : (abs x (var x)) =α (abs y (var y)) := by
+  have h : (abs y (var y)) = (abs y ((var x).rename x y)) := by grind [rename]
+  rw [h]
+  apply AlphaEquiv.abs_rename
+  simp only [vars]
+  decide
 
--- section 5.3.4 of TAPL
-example : (abs y (app x y))[x := (app y z : Term ℕ)] = (abs w (app (app y z) w)) := by
-  simp +instances [subst, fv, bv, vars, rename, instHasFreshNat, HasFresh.ofSucc,
-    instHasSubstitutionTerm]
+example : (abs y (var x)).subst x (app (var y) (var z)) = (abs w (app (var y) (var z))) := by
+  simp only [rename, subst, fv, vars]
+  decide
 
--- example : (abs 0 (abs 1 (app (var 0) (var 1)))) =α (abs 1 (abs 0 (app (var 1) (var 0)))) := by
+-- section 5.3.4 of TAPL
+example : (abs y (app (var x) (var y))).subst x (app (var y) (var z)) =
+    (abs w (app (app (var y) (var z)) (var w))) := by
+  simp only [subst, vars, rename]
+  decide
+
+example : (abs x (abs y (app (var x) (var y)))) =α (abs y (abs x (app (var y) (var x)))) := by
+  apply AlphaEquiv.abs (y := z)
+  · simp only [vars]
+    decide
+  simp only [rename]
+  apply AlphaEquiv.abs (y := w)
+  · simp only [vars]
+    decide
+  simp only [rename]
+  apply AlphaEquiv.refl
 
 end CslibTests