diff --git a/Cslib.lean b/Cslib.lean
index c0269e0bb..b690098ae 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -128,6 +128,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
 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.HML.LogicalEquivalence
 public import Cslib.Logics.LinearLogic.CLL.Basic
diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
index 364b7cf8f..5cdab218c 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
@@ -12,11 +12,14 @@ public import Cslib.Foundations.Syntax.HasSubstitution
 
 /-! # λ-calculus
 
-The untyped λ-calculus.
+The untyped λ-calculus, with a named representation of variables. This file contains the definitions
+of α-equivalence and capture-avoiding substitution.
 
 ## References
 
 * [H. Barendregt, *Introduction to Lambda Calculus*][Barendregt1984]
+* Definition of α-equivalence [M. Gabbay and A. Pitts, *A New Approach to Abstract Syntax with
+Variable Binding*][Gabbay2002]
 
 -/
 
@@ -26,9 +29,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
@@ -37,52 +40,75 @@ 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
+@[simp, scoped grind =]
+def fv : 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
+@[simp, scoped grind =]
+def bv : 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. -/
-def Term.vars [DecidableEq Var] (m : Term Var) : Finset Var :=
-  m.fv ∪ m.bv
+@[simp, scoped grind =]
+def vars : Term Var → Finset Var
+  | var x => {x}
+  | abs x m => m.vars ∪ {x}
+  | app m n => m.vars ∪ n.vars
 
-/-- 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')
-
-/-- Renaming, or variable substitution. `m.rename x y` renames `x` into `y` in `m`. -/
-def Term.rename [DecidableEq Var] (m : Term Var) (x y : Var) : Term 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 => 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)
+  | 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
+@[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])
 
+/-- α-equivalence. -/
+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 : HasAlphaEquiv (Term Var) where
+  AlphaEquiv := AlphaEquiv
+
+omit [HasFresh Var] in
+/-- Allow grind to recognise the notation of α-equivalence. -/
+@[simp, scoped grind _=_]
+theorem AlphaEquiv_def (m n : Term Var) : m =α n ↔ AlphaEquiv m n := by
+  rfl
+
+/-- Capture-avoiding substitution, as an inference system. -/
+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)
+  | 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`. -/
-def Term.subst [DecidableEq Var] [HasFresh Var] (m : Term Var) (x : Var) (r : Term Var) :
-  Term Var :=
+@[simp, scoped grind =]
+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' =>
@@ -91,25 +117,21 @@ 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
-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 [DecidableEq Var] [HasFresh Var] :
+instance instHasSubstitutionTerm :
     HasSubstitution (Term Var) Var (Term Var) where
-  subst := Term.subst
+  subst := 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
+/-- Allow grind to recognise the notation of substitution. -/
+@[simp, scoped grind _=_]
+theorem subst_def (m r : Term Var) (x : Var) : m[x := r] = m.subst x r := by
+  rfl
 
 /-- Contexts. -/
 inductive Context (Var : Type u) : Type u where
@@ -127,39 +149,13 @@ 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
+/-- Variables (both free and bound) in a context. -/
+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
new file mode 100644
index 000000000..dd98742b7
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
@@ -0,0 +1,514 @@
+/-
+Copyright (c) 2026 Haoxuan Yin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Haoxuan Yin, Fabrizio Montesi
+-/
+
+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
+
+universe u
+
+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
+
+/-- Renaming an unused variable has no effect. -/
+@[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, 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. -/
+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
+  | abs z m ih =>
+    intro hx
+    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
+    · grind
+
+/-- Renaming removes the variable. -/
+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]
+
+/-- 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
+  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 with
+  | var z => grind
+  | abs z m ih => grind [vars_either_fv_or_bv]
+  | app m n ihm ihn => grind
+
+/-- Concatenation of renaming. -/
+@[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} :
+    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
+  grind [rename_comm_fresh]
+
+omit [DecidableEq Var] in
+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
+  intro h
+  induction h with
+  | @var x => rfl
+  | @abs y x1 x2 m1 m2 hy h ih =>
+    simp
+    grind
+  | @app m1 n1 m2 n2 _ hm hn =>
+    grind
+
+/-- α-equivalent terms have the same free variables. -/
+theorem AlphaEquiv.same_fv {m n : Term Var} : m =α n → m.fv = n.fv := by
+  intro h
+  induction h with
+  | var => rfl
+  | app => grind
+  | @abs y x1 x2 m1 m2 hy h ih =>
+    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
+  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 => grind [AlphaEquiv.var]
+  | @abs y x1 x2 m1 m2 hy h ih =>
+    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
+  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,
+    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 {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 =>
+    by_cases hzy : z = y
+    · grind
+    · have hxzy : ((m1.rename x1 z).rename z y) =α ((m2.rename x2 z).rename z y) := by
+        grind [AlphaEquiv.rename_preserve]
+      grind
+
+/-- Transitivity of α-equivalence. -/
+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
+  intro hx hy
+  induction m with
+  | var z => grind [AlphaEquiv.var]
+  | app m1 m2 ih1 ih2 => grind [AlphaEquiv.app]
+  | abs z m ih =>
+    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⟩ := fresh_exists <| free_union [vars] Var
+  apply AlphaEquiv.abs (y := y)
+  · grind
+  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⟩ := 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
+  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]
+
+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]
+
+/-- α-equivalence is preserved under context filling. -/
+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
+  | abs x c ih =>
+    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]
+  | appR m c ih =>
+    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
+  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
+  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
+  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
+        · 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 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} →
+    ((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
+  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. -/
+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
+    | 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.eq_2, hyx, ↓reduceIte, hyr, not_false_eq_true, AlphaEquiv_def]
+      apply AlphaEquiv.context (c := Context.abs y Context.hole)
+      assumption
+    | @alpha m m' r r' n n' x hm hr hn h ih =>
+      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]
+
+/-- 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
+  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 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
+      grind [AlphaEquiv.trans]
+
+end LambdaCalculus.Named.Untyped.Term
+
+end Cslib
diff --git a/CslibTests/LambdaCalculus.lean b/CslibTests/LambdaCalculus.lean
index 1a331ea58..331516694 100644
--- a/CslibTests/LambdaCalculus.lean
+++ b/CslibTests/LambdaCalculus.lean
@@ -1,42 +1,55 @@
 /-
 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
 
+/-! # λ-calculus
 
+Tests for the named untyped λ-calculus.
 
-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]
+namespace CslibTests
 
-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
diff --git a/references.bib b/references.bib
index b2d78518f..b1a8c731a 100644
--- a/references.bib
+++ b/references.bib
@@ -131,6 +131,26 @@ @article{ FLP1985
   numpages  = {9}
 }
 
+@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},