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 01/14] 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 02/14] 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 03/14] 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 04/14] 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 05/14] 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 06/14] 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 07/14] 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 08/14] 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 09/14] 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

From 2ff6974f1160a97b2265cfb73d3c7cde180438b4 Mon Sep 17 00:00:00 2001
From: Haoxuan Yin <haoxn.yin@gmail.com>
Date: Tue, 7 Apr 2026 09:37:11 +0100
Subject: [PATCH 10/14] fix test failure again

---
 CslibTests/LambdaCalculus.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CslibTests/LambdaCalculus.lean b/CslibTests/LambdaCalculus.lean
index b0743e63e..dc4b598e5 100644
--- a/CslibTests/LambdaCalculus.lean
+++ b/CslibTests/LambdaCalculus.lean
@@ -5,7 +5,7 @@ Authors: Fabrizio Montesi, Haoxuan Yin
 -/
 
 import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
-import CsLib.Languages.LambdaCalculus.Named.Untyped.Properties
+import Cslib.Languages.LambdaCalculus.Named.Untyped.Properties
 
 namespace CslibTests
 

From f20561920acc0a8afb3d04fe98c02eba30f89465 Mon Sep 17 00:00:00 2001
From: Haoxuan Yin <haoxn.yin@gmail.com>
Date: Tue, 7 Apr 2026 23:15:20 +0100
Subject: [PATCH 11/14] fix grind annotation

---
 Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
index 1589c526e..714e22cc4 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
@@ -89,8 +89,8 @@ theorem rename_comm2 {m : Term Var} {x y z w : Var} :
   · 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
+@[grind norm↓← ]
+lemma induction_by_sizeOf {m n : Term Var} : sizeOf m < sizeOf n ↔ WellFoundedRelation.rel m n := by
   rfl
 
 /-- α-equivalent terms have the same size. -/
@@ -130,6 +130,7 @@ theorem AlphaEquiv.refl (m : Term Var) : m =α m := by
     apply AlphaEquiv.abs (y := z)
     · grind [rename_vars]
     apply ih
+    -- rw [← induction_by_sizeOf]
     grind [rename_eq_sizeOf]
   | app m n =>
     apply AlphaEquiv.app <;> apply ih <;> grind

From 1c9a553e64c03734ea642138e1734dea52ac90a0 Mon Sep 17 00:00:00 2001
From: Haoxuan Yin <haoxn.yin@gmail.com>
Date: Tue, 7 Apr 2026 23:35:35 +0100
Subject: [PATCH 12/14] cleanup

---
 Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
index 714e22cc4..4ad99a267 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
@@ -130,7 +130,6 @@ theorem AlphaEquiv.refl (m : Term Var) : m =α m := by
     apply AlphaEquiv.abs (y := z)
     · grind [rename_vars]
     apply ih
-    -- rw [← induction_by_sizeOf]
     grind [rename_eq_sizeOf]
   | app m n =>
     apply AlphaEquiv.app <;> apply ih <;> grind

From 6118958f597747689c57a149d5681fc1309d2056 Mon Sep 17 00:00:00 2001
From: Haoxuan Yin <haoxn.yin@gmail.com>
Date: Wed, 8 Apr 2026 08:48:31 +0100
Subject: [PATCH 13/14] fix linting error

---
 Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
index d43b04072..d6557d7f6 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
@@ -144,6 +144,7 @@ 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)
 
+/-- Variables (both free and bound) in a context. -/
 def Context.vars : Context Var → Finset Var
   | hole => ∅
   | abs x c => c.vars ∪ {x}

From 331cfd3d25af7834448041ca5615d1ea602a892b Mon Sep 17 00:00:00 2001
From: Haoxuan Yin <haoxn.yin@gmail.com>
Date: Wed, 27 May 2026 20:58:17 +0100
Subject: [PATCH 14/14] Change according to reviews. Add grind annotations and
 shorten proofs.

---
 .../LambdaCalculus/Named/Untyped/Basic.lean   |  21 +-
 .../Named/Untyped/Properties.lean             | 796 +++++++-----------
 CslibTests/LambdaCalculus.lean                |   6 +
 references.bib                                |  20 +
 4 files changed, 365 insertions(+), 478 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
index f0ed25982..5cdab218c 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
@@ -12,7 +12,8 @@ public import Cslib.Foundations.Syntax.HasSubstitution
 
 /-! # λ-calculus
 
-The untyped λ-calculus, with a named representation of variables.
+The untyped λ-calculus, with a named representation of variables. This file contains the definitions
+of α-equivalence and capture-avoiding substitution.
 
 ## References
 
@@ -42,18 +43,21 @@ deriving DecidableEq
 namespace Term
 
 /-- Free variables. -/
+@[simp, scoped grind =]
 def fv : Term Var → Finset Var
   | var x => {x}
   | abs x m => m.fv \ {x}
   | app m n => m.fv ∪ n.fv
 
 /-- Bound variables. -/
+@[simp, scoped grind =]
 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. -/
+@[simp, scoped grind =]
 def vars : Term Var → Finset Var
   | var x => {x}
   | abs x m => m.vars ∪ {x}
@@ -61,6 +65,7 @@ def vars : Term Var → Finset Var
 
 /-- Variable renaming, applying to both free and bound variables.
     `m.rename x y` changes all occurrences of `x` into `y` in `m`. -/
+@[simp, scoped grind =]
 def rename (m : Term Var) (x y : Var) : Term Var :=
   match m with
   | var z => var (if z = x then y else z)
@@ -69,7 +74,7 @@ def rename (m : Term Var) (x y : Var) : Term Var :=
 
 omit [HasFresh Var] in
 /-- Renaming preserves size. -/
-@[simp]
+@[simp, scoped grind =]
 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])
 
@@ -86,8 +91,8 @@ instance instHasAlphaEquivTerm : HasAlphaEquiv (Term Var) where
 
 omit [HasFresh Var] in
 /-- Allow grind to recognise the notation of α-equivalence. -/
-@[grind ←]
-theorem AlphaEquiv_def (m n : Term Var) : AlphaEquiv m n ↔ m =α n := by
+@[simp, scoped grind _=_]
+theorem AlphaEquiv_def (m n : Term Var) : m =α n ↔ AlphaEquiv m n := by
   rfl
 
 /-- Capture-avoiding substitution, as an inference system. -/
@@ -101,7 +106,7 @@ inductive Subst : Term Var → Var → Term Var → Term Var → Prop where
 
 /-- Capture-avoiding substitution. `m.subst x r` replaces the free occurrences of variable `x`
 in `m` with `r`. -/
-@[grind, simp]
+@[simp, scoped grind =]
 def subst (m : Term Var) (x : Var) (r : Term Var) :
     Term Var :=
   match m with
@@ -116,7 +121,7 @@ def subst (m : Term Var) (x : Var) (r : Term Var) :
       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
 
 /-- `Term.subst` is a substitution for λ-terms. Gives access to the notation `m[x := n]`. -/
 instance instHasSubstitutionTerm :
@@ -124,8 +129,8 @@ instance instHasSubstitutionTerm :
   subst := subst
 
 /-- Allow grind to recognise the notation of substitution. -/
-@[grind ←]
-theorem subst_def (m r : Term Var) (x : Var) : m.subst x r = m[x := r] := by
+@[simp, scoped grind _=_]
+theorem subst_def (m r : Term Var) (x : Var) : m[x := r] = m.subst x r := by
   rfl
 
 /-- Contexts. -/
diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
index 4ad99a267..dd98742b7 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
@@ -8,6 +8,23 @@ module
 
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
 
+
+/-! # λ-calculus
+
+The untyped λ-calculus, with a named representation of variables. This file contains properties of
+α-equivalence and capture-avoiding substitution.
+
+## Main results
+
+- `AlphaEquiv.refl`: reflexivity of α-equivalence
+- `AlphaEquiv.symm`: symmetry of α-equivalence
+- `AlphaEquiv.trans`: transitivity of α-equivalence
+- `Subst.relation_iff_function`: the relational and functional definition of capture-avoiding
+  substitution are equivalent, modulo alpha-equivalence
+- `subst.commutativity`: commutativity of substitution, more commonly known as the
+  "substitution lemma" (e.g. in [Barendregt1984])
+-/
+
 public section
 
 namespace Cslib
@@ -19,79 +36,75 @@ variable {Var : Type u} [DecidableEq Var]
 namespace LambdaCalculus.Named.Untyped.Term
 
 /-- A variable in a term is either free or bound. -/
-theorem vars_either_fv_or_bv {m : Term Var} :
-    m.vars = m.fv ∪ m.bv := by
-  induction m <;> grind [fv, bv, vars]
+theorem vars_either_fv_or_bv {m : Term Var} : m.vars = m.fv ∪ m.bv := by
+  induction m <;> grind
 
 /-- Renaming an unused variable has no effect. -/
-@[simp]
-theorem rename_unused {m : Term Var} {x y : Var} :
-  x ∉ m.vars → m.rename x y = m := by
-  induction m <;> grind [vars, rename]
+@[simp, scoped grind =]
+theorem rename_unused {m : Term Var} {x y : Var} : x ∉ m.vars → m.rename x y = m := by
+  induction m <;> grind
 
 /-- Renaming a variable to itself has no effect. -/
-@[simp]
-theorem rename_same {m : Term Var} {x : Var} :
-  m.rename x x = m := by
-  induction m <;> grind [vars, rename]
+@[simp, scoped grind =]
+theorem rename_same {m : Term Var} {x : Var} : m.rename x x = m := by
+  induction m <;> grind
 
 /-- Renaming a used variable changes the set of variables. -/
-@[simp]
-theorem rename_vars_used {m : Term Var} {x y : Var} :
-  x ∈ m.vars → (m.rename x y).vars = m.vars.erase x ∪ {y} := by
+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]
+  | var z => grind
   | abs z m ih =>
     intro hx
-    by_cases hxm : x ∈ m.vars <;> grind [vars, rename, rename_unused]
+    by_cases hxm : x ∈ m.vars <;> grind
   | app m n ihm ihn =>
     intro hx
     by_cases hxm : x ∈ m.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]
+    · by_cases hxn : x ∈ n.vars <;> grind
+    · grind
 
 /-- Renaming removes the variable. -/
-theorem rename_remove {m : Term Var} {x y : Var} :
-  x ≠ y → x ∉ (m.rename x y).vars := by
+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]
+  by_cases hx : x ∈ m.vars <;> grind [rename_vars_used]
 
 /-- The set of variables after renaming. -/
+@[simp, scoped grind =]
 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]
+    (m.rename x y).vars = m.vars \ {x} ∪ (if x ∈ m.vars then {y} else ∅) := by
+  grind [rename_vars_used]
 
 /-- The set of free variables after renaming. -/
 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]
+    y ∉ m.vars → (m.rename x y).fv = m.fv \ {x} ∪ (if x ∈ m.fv then {y} else ∅) := by
+  induction m with
+  | var z => grind
+  | abs z m ih => grind [vars_either_fv_or_bv]
+  | app m n ihm ihn => grind
 
 /-- Concatenation of renaming. -/
-@[simp]
-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, simpler version. -/
+@[simp, scoped grind =]
+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
+
+/-- Commutativity of renaming distinct variables. -/
+theorem rename_comm_fresh {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
+
+/-- Commutativity of renaming. -/
 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]
+  grind [rename_comm_fresh]
 
 omit [DecidableEq Var] in
-@[grind norm↓← ]
-lemma induction_by_sizeOf {m n : Term Var} : sizeOf m < sizeOf n ↔ WellFoundedRelation.rel m n := by
-  rfl
+theorem induction_by_sizeOf {C : Term Var → Prop}
+    (step : ∀ m : Term Var, (∀ m1 : Term Var, sizeOf m1 < sizeOf m → C m1) → C m ) :
+    ∀ m : Term Var, C m :=
+  WellFounded.fix (r := sizeOfWFRel.rel) sizeOfWFRel.wf step
 
 /-- α-equivalent terms have the same size. -/
 theorem AlphaEquiv.eq_sizeOf {m n : Term Var} : m =α n → sizeOf m = sizeOf n := by
@@ -99,7 +112,8 @@ theorem AlphaEquiv.eq_sizeOf {m n : Term Var} : m =α n → sizeOf m = sizeOf n
   induction h with
   | @var x => rfl
   | @abs y x1 x2 m1 m2 hy h ih =>
-    simpa using ih
+    simp
+    grind
   | @app m1 n1 m2 n2 _ hm hn =>
     grind
 
@@ -107,70 +121,61 @@ theorem AlphaEquiv.eq_sizeOf {m n : Term Var} : m =α n → sizeOf m = sizeOf n
 theorem AlphaEquiv.same_fv {m n : Term Var} : m =α n → m.fv = n.fv := by
   intro h
   induction h with
-  | @var x => rfl
+  | var => rfl
+  | app => grind
   | @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]
+    grind =>
+      instantiate [rename_fv, vars_either_fv_or_bv]
+      have : m1.fv \ {x1} = (m1.rename x1 y).fv \ {y}
+      have : (m2.rename x2 y).fv \ {y} = m2.fv \ {x2}
 
 variable [HasFresh Var]
 
 /-- Reflexivity of α-equivalence. -/
 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
-  | var x => apply AlphaEquiv.var
-  | abs x m =>
-    obtain ⟨z, hz⟩ := HasFresh.fresh_exists (m.vars ∪ {x})
-    apply AlphaEquiv.abs (y := z)
-    · grind [rename_vars]
-    apply ih
-    grind [rename_eq_sizeOf]
-  | app m n =>
-    apply AlphaEquiv.app <;> apply ih <;> grind
+  induction m using induction_by_sizeOf with
+  | step m ih =>
+    cases m with
+    | var x => grind [AlphaEquiv.var]
+    | abs x m =>
+      obtain ⟨z, hz⟩ := fresh_exists <| free_union [vars] Var
+      apply AlphaEquiv.abs (y := z) <;> grind
+    | app m n => grind [AlphaEquiv.app]
 
 omit [HasFresh Var] in
 /-- Symmetry of α-equivalence. -/
 theorem AlphaEquiv.symm {m n : Term Var} : m =α n → n =α m := by
   intro h
   induction h with
-  | @var x => apply AlphaEquiv.var
+  | @var x => grind [AlphaEquiv.var]
   | @abs y x1 x2 m1 m2 hy h 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
+    apply AlphaEquiv.abs (y := y) <;> grind
+  | @app m1 n1 m2 n2 hwm1 hwn1 hwm2 hwn2 => grind [AlphaEquiv.app]
 
 /-- Renaming α-equivalent terms produces α-equivalent terms. -/
 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
-  intro m ih n x y hy h
-  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)
-    · 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 <;> grind [vars]
+  induction m using induction_by_sizeOf generalizing n x y with
+  | step m ih =>
+    intro hy h
+    by_cases hyx : y = x
+    · grind
+    cases h with
+    | @var z => grind [AlphaEquiv.refl]
+    | @app m1 n1 m2 n2 hm hn => grind [AlphaEquiv.app]
+    | @abs z x1 x2 m1 m2 hz hbody =>
+      obtain ⟨w, hw⟩ := fresh_exists <| free_union [vars] Var
+      simp at hw hy
+      apply AlphaEquiv.abs (y := w)
+      · grind
+      rw [rename_comm, rename_comm]
+      case neg.abs.a =>
+        apply ih
+        · grind
+        · grind
+        · have hxzw : ((m1.rename x1 z).rename z w) =α ((m2.rename x2 z).rename z w) := by grind
+          grind
+      all_goals grind
 
 /-- Elimination rule for α-equivalence of abstractions.
     It states that if two abstractions are α-equivalent,
@@ -186,92 +191,70 @@ theorem AlphaEquiv.abs_elim {m1 m2 : Term Var} {x1 x2 y : Var} :
     by_cases hzy : z = y
     · grind
     · have hxzy : ((m1.rename x1 z).rename z y) =α ((m2.rename x2 z).rename z y) := by
-        apply AlphaEquiv.rename_preserve <;> grind [AlphaEquiv.rename_preserve, rename_vars]
-      grind [rename_concat, rename_vars]
+        grind [AlphaEquiv.rename_preserve]
+      grind
 
 /-- Transitivity of α-equivalence. -/
-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
-  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)
-        · 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 <;> grind [vars, rename_vars]
-        · apply ih _ ?_ n2 <;> grind [vars, rename_vars]
+theorem AlphaEquiv.trans {m n p : Term Var} : m =α n → n =α p → m =α p := by
+  induction m using induction_by_sizeOf generalizing n p with
+  | step m ih =>
+    intro hmn hnp
+    cases m with
+    | var x =>
+      cases hmn with
+      | @var x => assumption
+    | abs x1 m1 =>
+      obtain ⟨w, hw⟩ := fresh_exists <| free_union [vars] Var
+      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)
+          · grind
+          apply ih (n := m2.rename x2 w) <;> grind [AlphaEquiv.abs_elim]
+    | 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 (n := n1) <;> grind
+          · apply ih (n := n2) <;> grind
 
 /-- 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
+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
-      grind [fv]
-    simpa [rename, hzx] using AlphaEquiv.var
+  | var z => grind [AlphaEquiv.var]
+  | app m1 m2 ih1 ih2 => grind [AlphaEquiv.app]
   | 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)
-      · 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)
-      · 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]
+    obtain ⟨w, hw⟩ := fresh_exists <| free_union [vars] Var
+    apply AlphaEquiv.abs (y := w) <;> grind [AlphaEquiv.refl, AlphaEquiv.rename_preserve]
 
 /-- 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})
+  obtain ⟨y, hy⟩ := fresh_exists <| free_union [vars] Var
   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]
+  grind [AlphaEquiv.abs, AlphaEquiv.trans, rename_non_fv, AlphaEquiv.symm]
 
 /-- 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]
+  obtain ⟨z, hz⟩ := fresh_exists <| free_union [vars] Var
+  apply AlphaEquiv.abs (y := z) <;> grind [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) :
-    ∃ (c : Context Var) (x : Var), m = (c.fill (var x)) := by
+theorem Context.complete (m : Term Var) : ∃ (c : Context Var) (x : Var), m = (c.fill (var x)) := by
   induction m with
   | var x => exists hole, x
   | abs x n ih =>
@@ -285,9 +268,8 @@ theorem Context.complete (m : Term Var) :
 
 omit [HasFresh Var] in
 /-- The set of variables after filling a context. -/
-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]
+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]
 
 /-- α-equivalence is preserved under context filling. -/
 theorem AlphaEquiv.context {m n : Term Var} {c : Context Var} :
@@ -296,271 +278,185 @@ theorem AlphaEquiv.context {m n : Term Var} {c : Context Var} :
   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})
+    obtain ⟨y, hy⟩ := 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]
+    apply AlphaEquiv.app <;> grind [AlphaEquiv.app, AlphaEquiv.refl]
   | appR m c ih =>
-    apply AlphaEquiv.app <;> grind [AlphaEquiv.app, AlphaEquiv.refl, vars]
+    apply AlphaEquiv.app <;> grind [AlphaEquiv.app, AlphaEquiv.refl]
 
 /-- 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
-  | var y =>
-    by_cases hyx : y = x
-    · subst y
-      simp only [← subst_def, subst.eq_1, ↓reduceIte]
-      apply Subst.varHit
-    · simp [hyx, ← subst_def]
-      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
+theorem Subst.function_to_relation {m r : Term Var} {x : Var} : m.Subst x r (m[x := r]) := by
+  induction m using induction_by_sizeOf with
+  | step m ih =>
+    cases m with
+    | var y => grind [Subst.varHit, Subst.varMiss]
+    | app m1 m2 => grind [Subst.app]
+    | abs y m =>
+      by_cases hyx : y = x
+      · grind [Subst.absShadow]
+      · by_cases hyr : y ∈ r.fv
+        · let s := {x, y} ∪ m.vars ∪ r.vars
+          have hz := fresh_notMem s
+          set z := fresh s
+          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
+            grind [AlphaEquiv.symm, AlphaEquiv.rename_non_fv]
+          · grind [AlphaEquiv.refl]
+          · grind [AlphaEquiv.refl]
+          · grind [Subst.absIn, vars_either_fv_or_bv]
+        · grind [Subst.absIn]
 
 /-- 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
-  | 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]
-
-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]))
+theorem subst.non_free {m r : Term Var} {x : Var} : x ∉ m.fv → (m[x := r]) =α m := by
+  induction m using induction_by_sizeOf with
+  | step m ih =>
+    intro hx
+    cases m with
+    | var y => grind [AlphaEquiv.var]
+    | app m1 m2 => grind [AlphaEquiv.app]
+    | abs y m =>
+      by_cases hyx : y = x
+      · grind [AlphaEquiv.refl]
+      · by_cases hyr : y ∈ r.fv
+        · simp only [subst_def, eq_2, hyx, ↓reduceIte, hyr, not_true_eq_false, Finset.union_insert,
+            Finset.union_singleton, AlphaEquiv_def]
+          let s := (insert x (insert y (m.vars ∪ r.vars)))
+          have hz := fresh_notMem s
+          set z := fresh s
+          obtain ⟨w, hw⟩ := fresh_exists (m.vars ∪ r.vars ∪ ((m.rename y z).subst x r).vars
+            ∪ {x, y, z})
+          apply AlphaEquiv.abs (y := w)
+          · grind
+          apply AlphaEquiv.trans (n := ((m.rename y z).rename z w))
+          · grind [AlphaEquiv.rename_preserve, rename_fv]
+          · grind [AlphaEquiv.refl]
+        · simp only [subst_def, eq_2, hyx, ↓reduceIte, hyr, not_false_eq_true, AlphaEquiv_def]
+          apply AlphaEquiv.context (c := Context.abs y Context.hole)
+          grind
+
+private 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} →
-    ((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
-    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 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'
-        · 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 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
-        ∪ 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 AlphaEquiv.abs_non_fv
-        · apply (ih _ _ _ _ _ _ _).right <;> grind [vars]
-        · grind [fv]
-        · grind [fv]
-      · rw [rename]
-        simp only [hwy', ↓reduceIte]
+  induction m using induction_by_sizeOf generalizing r x y z with
+  | step m ih =>
+    intro 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
-          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 : (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 ∪
-                ((m1.rename w v).rename y' z)[x:=r].vars ∪ {y', z})
-              apply AlphaEquiv.abs (y := u)
+        · grind [vars_either_fv_or_bv, AlphaEquiv.refl, AlphaEquiv.abs_non_fv]
+        · by_cases hwy' : w = y'
+          · obtain ⟨v, hv⟩ := fresh_exists <| free_union [vars] Var
+            apply AlphaEquiv.abs (y := v) <;> grind [AlphaEquiv.var]
+          · grind [vars_either_fv_or_bv, AlphaEquiv.refl, AlphaEquiv.abs_non_fv]
+      | app m1 m2 =>
+        obtain ⟨w, hw⟩ := 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 [AlphaEquiv.app, AlphaEquiv.abs_elim]
+      | abs w m1 =>
+        by_cases hwy' : w = y'
+        · grind [vars_either_fv_or_bv, AlphaEquiv.abs_non_fv]
+        · rw [rename]
+          simp only [hwy', ↓reduceIte]
+          by_cases hwx : w = x
+          · grind [AlphaEquiv.trans, AlphaEquiv.abs_rename, AlphaEquiv.refl]
+          · by_cases hwr : w ∈ r.fv
+            · obtain ⟨v, hv⟩ := fresh_exists <| free_union [vars] Var
+              simp at hv
+              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)
+                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)
+                grind [AlphaEquiv.symm]
+              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⟩ := 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)
+                  grind [AlphaEquiv.trans, AlphaEquiv.abs_elim, AlphaEquiv.rename_preserve,
+                    rename_comm_fresh, AlphaEquiv.refl]
+              grind [AlphaEquiv.trans]
+            · obtain ⟨v, hv⟩ := 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
-              · 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 AlphaEquiv.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 := (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]
-          · 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)⟩
+              · have hwz : w ≠ z := by grind
+                simp only [subst_def, eq_2, hwx, ↓reduceIte, hwr, not_false_eq_true, rename, hwy',
+                  hwz]
+                apply AlphaEquiv.context (c := Context.abs w Context.hole)
+                grind [AlphaEquiv.abs_elim]
+    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, eq_2, ↓reduceIte, AlphaEquiv_def]
+        obtain ⟨w, hw⟩ := fresh_exists (m.vars ∪ r.vars ∪ ((m.rename x z).subst x r).vars ∪
+          {x, z})
+        apply AlphaEquiv.abs (y := w)
+        · grind
+        · apply AlphaEquiv.trans (n := ((m.rename x z).rename z w))
+          · grind [AlphaEquiv.refl]
+          · grind [AlphaEquiv.rename_preserve, AlphaEquiv.symm, subst.non_free, rename_fv]
+      · by_cases hyr : y ∈ r.fv
+        · simp only [subst_def, eq_2, hyx, ↓reduceIte, hyr, not_true_eq_false, Finset.union_insert,
+              Finset.union_singleton, AlphaEquiv_def]
+          let s := (insert x (insert y (m.vars ∪ r.vars)))
+          have hw := fresh_notMem s
+          set w := fresh s
+          grind [AlphaEquiv.refl, AlphaEquiv.trans, vars_either_fv_or_bv]
+        · grind
+    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 subst.abs_fresh {m r : Term Var} {x y z : Var} :
-    z ∉ m.vars ∪ r.vars ∪ {x, y} →
+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 {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 : ((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 :
-        (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
-    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 =>
-    simp only [← subst_def, subst]
-    apply AlphaEquiv.app <;> apply ih <;> grind
+  induction m using induction_by_sizeOf generalizing m' r r' x with
+  | step m ih =>
+    intro hmm' hrr'
+    have hmm'' := hmm'
+    cases hmm'' with
+    | @var y => grind [AlphaEquiv.refl]
+    | @app m m' n n' hm hn => grind [AlphaEquiv.app]
+    | @abs z y y' m m' hz h1 =>
+      obtain ⟨w, hw⟩ := fresh_exists <| free_union [vars] Var
+      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 :
+          (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]
+      grind [AlphaEquiv.trans, AlphaEquiv.symm]
 
 /-- The relational definition of substitution coincides with the functional definition of
     substitution, modulo α-equivalence. -/
@@ -569,28 +465,18 @@ theorem Subst.relation_iff_function {m n r : Term Var} {x : Var} :
   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
+    | varHit => grind [AlphaEquiv.refl]
+    | varMiss => grind [AlphaEquiv.refl]
+    | absShadow => grind [AlphaEquiv.refl]
+    | app => grind [AlphaEquiv.app]
     | @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]
+      simp only [subst_def, subst.eq_2, hyx, ↓reduceIte, hyr, not_false_eq_true, AlphaEquiv_def]
       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]
+      grind [AlphaEquiv.symm, AlphaEquiv.trans, 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]
@@ -598,60 +484,30 @@ theorem Subst.relation_iff_function {m n r : Term Var} {x : Var} :
 /-- Commutativity of substitution (a.k.a. the substitution lemma) -/
 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} →
-      ((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]
+  induction m using induction_by_sizeOf generalizing r1 r2 x y with
+  | step m ih =>
+    intro hx
+    cases m with
+    | var z => grind [AlphaEquiv.refl, AlphaEquiv.symm, subst.non_free]
+    | app m1 m2 => grind [AlphaEquiv.app]
+    | abs z m =>
+      obtain ⟨w, hw⟩ := 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])))
+        · grind [subst.preserve_AlphaEquiv, subst.abs_fresh, AlphaEquiv.refl]
+        · grind [vars_either_fv_or_bv, 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 subst.non_free
+        apply AlphaEquiv.trans (n := ((Term.abs w ((m.rename z w)[y := r2]))[x := (r1[y := r2])]))
+        · grind [subst.preserve_AlphaEquiv, subst.abs_fresh, AlphaEquiv.refl]
+        · grind [vars_either_fv_or_bv, 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)
         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 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 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
+      grind [AlphaEquiv.trans]
 
 end LambdaCalculus.Named.Untyped.Term
 
diff --git a/CslibTests/LambdaCalculus.lean b/CslibTests/LambdaCalculus.lean
index dc4b598e5..331516694 100644
--- a/CslibTests/LambdaCalculus.lean
+++ b/CslibTests/LambdaCalculus.lean
@@ -7,6 +7,12 @@ Authors: Fabrizio Montesi, Haoxuan Yin
 import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
 import Cslib.Languages.LambdaCalculus.Named.Untyped.Properties
 
+/-! # λ-calculus
+
+Tests for the named untyped λ-calculus.
+
+-/
+
 namespace CslibTests
 
 open Cslib Cslib.LambdaCalculus.Named.Untyped.Term
diff --git a/references.bib b/references.bib
index f0d122d17..0fce13eb9 100644
--- a/references.bib
+++ b/references.bib
@@ -101,6 +101,26 @@ @article{         Chargueraud2012
 	file = {Full Text PDF:/home/chenson/mount/Zotero/storage/WBJWAZGI/Charguéraud - 2012 - The Locally Nameless Representation.pdf:application/pdf},
 }
 
+@article{Gabbay2002,
+author = {Gabbay, Murdoch J. and Pitts, Andrew M.},
+title = {A New Approach to Abstract Syntax with Variable Binding},
+year = {2002},
+issue_date = {Jul 2002},
+publisher = {Springer-Verlag},
+address = {Berlin, Heidelberg},
+volume = {13},
+number = {3–5},
+issn = {0934-5043},
+url = {https://doi.org/10.1007/s001650200016},
+doi = {10.1007/s001650200016},
+abstract = {The permutation model of set theory with atoms (FM-sets), devised by Fraenkel and Mostowski in the 1930s, supports notions of ‘name-abstraction’ and ‘fresh name’ that provide a new way to represent, compute with, and reason about the syntax of formal systems involving variable-binding operations. Inductively defined FM-sets involving the name-abstraction set former (together with Cartesian product and disjoint union) can correctly encode syntax modulo renaming of bound variables. In this way, the standard theory of algebraic data types can be extended to encompass signatures involving binding operators. In particular, there is an associated notion of structural recursion for defining syntax-manipulating functions (such as capture avoiding substitution, set of free variables, etc.) and a notion of proof by structural induction, both of which remain pleasingly close to informal practice in computer science.},
+journal = {Form. Asp. Comput.},
+month = jul,
+pages = {341–363},
+numpages = {23},
+keywords = {Keywords: Abstract syntax; Alpha-conversion; Permutation actions; Set theory; Structural induction}
+}
+
 @article{        Girard1987,
   title={Linear logic},
   author={Girard, Jean-Yves},