diff --git a/Cslib.lean b/Cslib.lean
index f21b49009..5d1d60ac4 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -157,8 +157,12 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StandardReduction
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.AlphaEquivDefs
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.AlphaEquivEquiv
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.AlphaEquivProperties
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
-public import Cslib.Languages.LambdaCalculus.Named.Untyped.Properties
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.RenameProperties
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.SwapProperties
 public import Cslib.Languages.Mech.Choreography.Basic
 public import Cslib.Languages.Mech.LocalComputation
 public import Cslib.Languages.StatefulProcesses.Basic
diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/AlphaEquivDefs.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/AlphaEquivDefs.lean
new file mode 100644
index 000000000..d71e018ee
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/AlphaEquivDefs.lean
@@ -0,0 +1,142 @@
+/-
+Copyright (c) 2026 Chris Anto Fröschl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Anto Fröschl
+-/
+
+module
+
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
+
+/-! # Definitions of α-equivalence
+
+Five definitions of α-equivalence from [Crole2012], each capturing the same equivalence
+relation on expressions:
+
+* `∼p`  (Definition 3.1): Permutation-based with non-occurrence side condition (`AlphaEquiv`)
+* `∼p#` (Definition 3.2): Permutation-based with freshness side condition (`AlphaEquivPFresh`)
+* `∼¹p` (Definition 3.3): Permutation-based with non-occurrence on bodies only (`AlphaEquivP1`)
+* `∼r`  (Definition 3.4): Traditional renaming axiom with non-occurrence (`AlphaEquivR`)
+* `∼r#` (Definition 3.5): Renaming axiom with freshness (`AlphaEquivRFresh`)
+
+The first three definitions use the notion of *atom swapping* (transposition), introduced in
+[Gabbay2002] (Section 2, page 3), as a primitive operation for defining α-equivalence. The
+key observation from [Gabbay2002] is that α-equivalence can be defined using the notion of
+atom swapping in lieu of the traditional renaming/substitution approach.
+
+The last two definitions use the traditional capture-avoiding substitution (renaming) axiom.
+
+## References
+
+* [Roy L. Crole, *Alpha equivalence equalities*][Crole2012]
+* [M. Gabbay and A. Pitts, *A New Approach to Abstract Syntax with Variable Binding*][Gabbay2002]
+
+## Notation
+
+Following the paper [Crole2012], we use the following correspondence between the paper's
+abstract syntax and the λ-calculus terms:
+
+| Paper         | Lean                |
+|---------------|---------------------|
+| `a`           | `Term.var x`        |
+| `P(E₁, E₂)`   | `Term.app m1 m2`    |
+| `B([a]E)`     | `Term.abs x m`      |
+| `(z a) · E`   | `m.swap x z`        |
+| `E{a'/a}`     | `m.subst a (var a')`|
+| `π · E`       | `m.permute π`       |
+-/
+
+@[expose] public section
+
+namespace Cslib
+
+universe u
+
+variable {Var : Type u} [DecidableEq Var] [HasFresh Var]
+
+namespace LambdaCalculus.Named.Untyped.Term
+
+/-- **Definition 3.2** [Crole2012]: `∼p#` - α-equivalence via permutation with freshness
+side condition.
+
+The rule `pi#` uses the freshness condition `z # a, b, E, E'`
+(i.e., `z ∉ fv(E) ∪ fv(E') ∪ {a, b}`) instead of the non-occurrence condition
+`z ∉ vars(E) ∪ vars(E') ∪ {a, b}` used in Definition 3.1 (`AlphaEquiv`).
+-/
+inductive AlphaEquivPFresh : Term Var → Term Var → Prop where
+  | var {x : Var} : AlphaEquivPFresh (var x) (var x)
+  | abs {y x1 x2 : Var} {m1 m2 : Term Var} :
+    y ∉ ({x1, x2} : Finset Var) ∪ m1.fv ∪ m2.fv →
+    AlphaEquivPFresh (m1.swap x1 y) (m2.swap x2 y) →
+    AlphaEquivPFresh (abs x1 m1) (abs x2 m2)
+  | app {m1 n1 m2 n2 : Term Var} :
+    AlphaEquivPFresh m1 n1 → AlphaEquivPFresh m2 n2 →
+    AlphaEquivPFresh (app m1 m2) (app n1 n2)
+
+/-- **Definition 3.3** [Crole2012]: `∼¹p` - α-equivalence via permutation with non-occurrence
+restricted to the bodies only.
+
+This definition is analogous to the definition of α-equivalence for λ-expressions in
+[Gabbay1999a] (Theorem 2.1, page 216). The notation `∼¹p` arises from three variants `∼ⁱp`
+of `∼p` considered in Proposition 4.3 of [Crole2012].
+-/
+inductive AlphaEquivP1 : Term Var → Term Var → Prop where
+  | var {x : Var} : AlphaEquivP1 (var x) (var x)
+  | abs {y x1 x2 m1 m2} :
+    y ∉ m1.vars ∪ m2.vars →
+    AlphaEquivP1 (m1.rename x1 y) (m2.rename x2 y) →
+    AlphaEquivP1 (abs x1 m1) (abs x2 m2)
+  | app {m1 n1 m2 n2 : Term Var} :
+    AlphaEquivP1 m1 n1 → AlphaEquivP1 m2 n2 →
+    AlphaEquivP1 (app m1 m2) (app n1 n2)
+
+/-- **Definition 3.4** [Crole2012]: `∼r` - α-equivalence via the traditional renaming axiom
+with non-occurrence side condition.
+
+This definition is analogous to the definition of α-equivalence for λ-expressions most commonly
+found in the literature. One of the first formal presentations is in [Church1941] and the same,
+though rather less formal approach is taken by [Barendregt1985] (Definition 2.1.11).
+-/
+inductive AlphaEquivR : Term Var → Term Var → Prop where
+  | refl {m : Term Var} : AlphaEquivR m m
+  | symm {m1 m2 : Term Var} : AlphaEquivR m1 m2 → AlphaEquivR m2 m1
+  | trans {m1 m2 m3 : Term Var} : AlphaEquivR m1 m2 → AlphaEquivR m2 m3 → AlphaEquivR m1 m3
+  | app {m1 n1 m2 n2 : Term Var} :
+    AlphaEquivR m1 n1 → AlphaEquivR m2 n2 →
+    AlphaEquivR (app m1 m2) (app n1 n2)
+  | abs_congr {x : Var} {m m' : Term Var} :
+    AlphaEquivR m m' →
+    AlphaEquivR (abs x m) (abs x m')
+  | alpha {x x' : Var} {m : Term Var} :
+    x' ∉ ({x} : Finset Var) ∪ m.vars →
+    AlphaEquivR (abs x m) (abs x' (m.subst x (var x')))
+
+/-- **Definition 3.5** [Crole2012]: `∼r#` - α-equivalence via the renaming axiom with
+freshness side condition.
+
+Same as `∼r` (Definition 3.4), but the renaming axiom uses a freshness side condition
+(`a' ∉ {a} ∪ fv(E)`) instead of a non-occurrence condition (`a' ∉ {a} ∪ vars(E)`).
+
+This is analogous to the definition of α-equivalence for λ-expressions one finds in
+[Hindley1988] (Section 1B, page 9).
+-/
+inductive AlphaEquivRFresh : Term Var → Term Var → Prop where
+  | refl {m : Term Var} : AlphaEquivRFresh m m
+  | symm {m1 m2 : Term Var} :
+    AlphaEquivRFresh m1 m2 → AlphaEquivRFresh m2 m1
+  | trans {m1 m2 m3 : Term Var} :
+    AlphaEquivRFresh m1 m2 → AlphaEquivRFresh m2 m3 →
+    AlphaEquivRFresh m1 m3
+  | app {m1 m1' m2 m2' : Term Var} :
+    AlphaEquivRFresh m1 m1' → AlphaEquivRFresh m2 m2' →
+    AlphaEquivRFresh (app m1 m2) (app m1' m2')
+  | abs_congr {x : Var} {m m' : Term Var} :
+    AlphaEquivRFresh m m' →
+    AlphaEquivRFresh (abs x m) (abs x m')
+  | alpha {x x' : Var} {m : Term Var} :
+    x' ∉ ({x} : Finset Var) ∪ m.fv →
+    AlphaEquivRFresh (abs x m) (abs x' (m.subst x (var x')))
+
+end LambdaCalculus.Named.Untyped.Term
+
+end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/AlphaEquivEquiv.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/AlphaEquivEquiv.lean
new file mode 100644
index 000000000..40e99c37f
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/AlphaEquivEquiv.lean
@@ -0,0 +1,131 @@
+/-
+Copyright (c) 2026 Chris Anto Fröschl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Anto Fröschl
+-/
+
+module
+
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.AlphaEquivDefs
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.RenameProperties
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.AlphaEquivProperties
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.SwapProperties
+
+/-! # Equivalence of α-equivalence definitions
+
+Theorems showing equivalence of the five definitions of α-equivalence from [Crole2012]:
+
+* `∼p`  (Definition 3.1): permutation with non-occurrence side condition (`AlphaEquiv`)
+* `∼p#` (Definition 3.2): permutation with freshness side condition (`AlphaEquivPFresh`)
+* `∼¹p` (Definition 3.3): permutation with non-occurrence on bodies only (`AlphaEquivP1`)
+* `∼r`  (Definition 3.4): traditional renaming axiom with non-occurrence (`AlphaEquivR`)
+* `∼r#` (Definition 3.5): renaming axiom with freshness (`AlphaEquivRFresh`)
+
+The main results are:
+
+* **Theorem 4.1** [Crole2012]: `∼p = ∼p#` (`alphaEquiv_iff_alphaEquivPFresh`)
+* **Theorem 4.2** [Crole2012]: `∼p = ∼¹p` (`alphaEquiv_iff_alphaEquivP1`)
+* **Theorem 4.4** [Crole2012]: `∼p = ∼r`  (`alphaEquiv_iff_alphaEquivR`)
+* **Theorem 4.5** [Crole2012]: `∼p = ∼r#` (`alphaEquiv_iff_alphaEquivRFresh`)
+* **Theorem 4.6** [Crole2012]: `∼r = ∼r#` (`alphaEquivR_iff_alphaEquivRFresh`)
+
+## References
+
+* [Roy L. Crole, *Alpha equivalence equalities*][Crole2012]
+-/
+
+@[expose] public section
+
+namespace Cslib
+
+universe u
+
+variable {Var : Type u} [DecidableEq Var] [HasFresh Var]
+
+namespace LambdaCalculus.Named.Untyped.Term
+
+omit [HasFresh Var] in
+/-- Non-occurrence obviously implies freshness, and the `swap` operation coincides with
+`rename` when the target variable does not occur in the term.
+-/
+lemma alphaEquiv_of_alphaEquivPFresh {m n : Term Var} : AlphaEquiv m n → AlphaEquivPFresh m n := by
+  intro h
+  induction h with
+  | var => constructor
+  | abs z_h1 ih1 ih2 =>
+    rename_i x z x1 x2 m1 m2
+    have h1 : z ∉ ({x1, x2} : Finset Var) ∪ m1.fv ∪ m2.fv := by
+      simp_all [vars_either_fv_or_bv]
+    have h2 : AlphaEquivPFresh (m1.swap x1 z) (m2.swap x2 z) := by
+      grind [swap_eq_rename_of_not_mem_vars]
+    apply AlphaEquivPFresh.abs h1 h2
+  | app h1 h2 ih1 ih2 => exact AlphaEquivPFresh.app ih1 ih2
+
+lemma alphaEquivPFresh_of_alphaEquiv {m n : Term Var} : AlphaEquivPFresh m n → AlphaEquiv m n := by
+  intro h
+  induction h with
+  | var => constructor
+  | abs hy _h ih =>
+    rename_i u a b E E'
+    -- We have: (u a) · E ∼p (u b) · E' (by induction: ih) and u # a, b, E, E' (by hy).
+    -- Extract freshness conditions from hy.
+    have hu_E : u ∉ E.fv := by aesop
+    have hu_E' : u ∉ E'.fv := by aesop
+    -- Pick z ≠ u with z ∉ vars(E) ∪ vars(E') ∪ {a, b} (stronger than freshness).
+    obtain ⟨z, hz⟩ : ∃ z : Var, z ∉ E.vars ∪ E'.vars ∪ {a, b, u} := by
+      exact Infinite.exists_notMem_finset (E.vars ∪ E'.vars ∪ {a, b, u})
+    have hz_E : z ∉ E.vars := by aesop
+    have hz_E' : z ∉ E'.vars := by aesop
+    have hz_fv_E : z ∉ E.fv := by simp_all [vars_either_fv_or_bv]
+    have hz_fv_E' : z ∉ E'.fv := by simp_all [vars_either_fv_or_bv]
+    -- Using Lemma 6.1 we get
+    have h_swap : ((E.swap u a).swap z u) =α ((E'.swap u b).swap z u) := by
+      nth_rw 2 [swap_comm]
+      nth_rw 4 [swap_comm]
+      exact AlphaEquiv.swap_preserve ih
+    -- From Lemma 6.2 part 2 via agreement sets
+    have h_agree_E : ((E.swap u a).swap z u) =α (E.swap z a) :=
+      swap_comp_alphaEquiv_of_not_mem_fv hu_E hz_fv_E
+    have h_agree_E' : ((E'.swap u b).swap z u) =α (E'.swap z b) :=
+      swap_comp_alphaEquiv_of_not_mem_fv hu_E' hz_fv_E'
+    -- Chain by symmetry and transitivity of ∼p
+    -- (z a) · E ∼p (z u)·(u a)·E ∼p (z u)·(u b)·E' ∼p (z b) · E'
+    have h_chain : (E.swap z a) =α (E'.swap z b) :=
+      AlphaEquiv.trans (AlphaEquiv.symm h_agree_E) (AlphaEquiv.trans h_swap h_agree_E')
+    -- Convert swap to rename (since z ∉ vars) and apply the pi rule.
+    -- Since z ∉ vars(E), swap z a = rename a z (by swap_comm + swap_eq_rename).
+    rw [swap_comm, swap_eq_rename_of_not_mem_vars hz_E] at h_chain
+    rw [swap_comm, swap_eq_rename_of_not_mem_vars hz_E'] at h_chain
+    exact AlphaEquiv.abs (by aesop) h_chain
+  | app _ _ ih1 ih2 => exact AlphaEquiv.app ih1 ih2
+
+/-! ## Theorem 4.1 [Crole2012] -/
+theorem alphaEquiv_iff_alphaEquivPFresh (m n : Term Var) : AlphaEquiv m n ↔ AlphaEquivPFresh m n :=
+  ⟨alphaEquiv_of_alphaEquivPFresh, alphaEquivPFresh_of_alphaEquiv⟩
+
+/-
+/-! ## Theorem 4.2 [Crole2012] -/
+theorem alphaEquiv_iff_alphaEquivP1 (m n : Term Var) :
+    AlphaEquiv m n ↔ AlphaEquivP1 m n := by
+  sorry
+
+/-! ## Theorem 4.4 [Crole2012] -/
+theorem alphaEquiv_iff_alphaEquivR (m n : Term Var) :
+    AlphaEquiv m n ↔ AlphaEquivR m n := by
+  sorry
+
+/-! ## Theorem 4.5 [Crole2012] -/
+theorem alphaEquiv_iff_alphaEquivRFresh (m n : Term Var) :
+    AlphaEquiv m n ↔ AlphaEquivRFresh m n := by
+  sorry
+
+/-! ## Theorem 4.6 [Crole2012] -/
+theorem alphaEquivR_iff_alphaEquivRFresh (m n : Term Var) :
+    AlphaEquivR m n ↔ AlphaEquivRFresh m n := by
+  sorry
+-/
+
+end LambdaCalculus.Named.Untyped.Term
+
+end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/AlphaEquivProperties.lean
similarity index 87%
rename from Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
rename to Cslib/Languages/LambdaCalculus/Named/Untyped/AlphaEquivProperties.lean
index dd98742b7..144bc97a6 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/AlphaEquivProperties.lean
@@ -1,15 +1,15 @@
 /-
 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
+Authors: Haoxuan Yin, Fabrizio Montesi, Chris Anto Fröschl
 -/
 
 module
 
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.RenameProperties
 
-
-/-! # λ-calculus
+/-! # Properties of α-equivalence
 
 The untyped λ-calculus, with a named representation of variables. This file contains properties of
 α-equivalence and capture-avoiding substitution.
@@ -35,77 +35,6 @@ 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
@@ -177,6 +106,14 @@ theorem AlphaEquiv.rename_preserve (m n : Term Var) (x y : Var) :
           grind
       all_goals grind
 
+lemma AlphaEquiv.abs_congr {m m' : Term Var} {x : Var} :
+    m =α m' → (Term.abs x m) =α (Term.abs x m') := by
+  intro h
+  obtain ⟨y, hy⟩ := HasFresh.fresh_exists (m.vars ∪ m'.vars ∪ {x})
+  apply AlphaEquiv.abs (y := y)
+  · simp_all
+  · apply AlphaEquiv.rename_preserve <;> 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.
diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
index 5cdab218c..d04873977 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean
@@ -19,8 +19,9 @@ of α-equivalence and capture-avoiding substitution.
 
 * [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]
-
+  Variable Binding*][Gabbay2002]
+* [Roy L. Crole, *Alpha equivalence equalities*][Crole2012] - the `AlphaEquiv` definition
+  corresponds to Definition 3.1 (∼p) in this paper
 -/
 
 @[expose] public section
@@ -63,6 +64,25 @@ def vars : Term Var → Finset Var
   | abs x m => m.vars ∪ {x}
   | app m n => m.vars ∪ n.vars
 
+/-- The action `π · E` of a permutation on a term, as used in [Crole2012].
+
+Since some lemmas in section 6 are proven for general permutations, we have to introduce
+this notion here aswell and derive the special case using `swap` accordingly.
+-/
+def permute (m : Term Var) (π : Equiv.Perm Var) : Term Var :=
+  match m with
+  | var x => var (π x)
+  | abs x m => abs (π x) (m.permute π)
+  | app m n => app (m.permute π) (n.permute π)
+
+/-- The action of the transposition `(x y)` on a term: simultaneously swaps all occurrences
+of `x` and `y`. Corresponds to `(x y) · E` in [Crole2012] (Section 2).
+
+`swap` is is one special case of a permutation: the transposition that exchanges exactly two atoms
+a and b and fixes everything else.
+-/
+def swap (m : Term Var) (x y : Var) : Term Var := m.permute (Equiv.swap x y)
+
 /-- 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 =]
@@ -72,13 +92,12 @@ def rename (m : Term Var) (x y : Var) : Term Var :=
   | 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, 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])
+/-- **Definition 3.1** [Crole2012]: `∼p` - α-equivalence via permutation (swapping) with
+non-occurrence side condition.
 
-/-- α-equivalence. -/
+This definition is analogous to the definition of α-equivalence for λ-expressions in
+[Gabbay2002] (Section 2, page 3). The `abs` rule uses the `rename` operation, which
+coincides with `swap` when the witness variable `y` does not occur in the term. -/
 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} →
@@ -104,6 +123,12 @@ inductive Subst : Term Var → Var → Term Var → Term Var → Prop where
   | 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'
 
+omit [HasFresh Var] in
+/-- Renaming preserves size. -/
+@[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])
+
 /-- Capture-avoiding substitution. `m.subst x r` replaces the free occurrences of variable `x`
 in `m` with `r`. -/
 @[simp, scoped grind =]
diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/RenameProperties.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/RenameProperties.lean
new file mode 100644
index 000000000..196babd02
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/RenameProperties.lean
@@ -0,0 +1,100 @@
+/-
+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
+
+/-! # Properties of rename
+
+The untyped λ-calculus, with a named representation of variables. This file contains properties of
+α-equivalence and capture-avoiding substitution.
+-/
+
+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
+
+end LambdaCalculus.Named.Untyped.Term
+
+end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/SwapProperties.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/SwapProperties.lean
new file mode 100644
index 000000000..6de024441
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/SwapProperties.lean
@@ -0,0 +1,511 @@
+/-
+Copyright (c) 2026 Chris Anto Fröschl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Anto Fröschl
+-/
+
+module
+
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.AlphaEquivProperties
+
+/-! # Properties of the swap (transposition) operation on lambda terms
+
+Helper lemmas for reasoning about `Term.swap` and its interaction with
+`AlphaEquiv`, `rename`, `vars`, and `fv`.
+
+The notion of *atom swapping* (transposition) as the basis for defining α-equivalence
+originates from [Gabbay and Pitts, *A New Approach to Abstract Syntax with Variable
+Binding*][Gabbay2002] (Section 2, page 3). The key observation is that α-equivalence can
+be defined using the notion of atom swapping in lieu of the traditional
+renaming/substitution approach.
+
+The swap (transposition) operation `m.swap x y` implements the permutation action
+`(x y) · E` from [Crole2012] (Section 2). It simultaneously replaces all occurrences
+of `x` with `y` and vice versa throughout a term.
+
+## References
+
+* [Roy L. Crole, *Alpha equivalence equalities*][Crole2012], Sections 2 and 6
+* [M. Gabbay and A. Pitts, *A New Approach to Abstract Syntax with Variable
+  Binding*][Gabbay2002], Section 2
+-/
+
+@[expose] public section
+
+namespace Cslib
+
+universe u
+
+variable {Var : Type u} [DecidableEq Var]
+
+namespace LambdaCalculus.Named.Untyped.Term
+
+/-- The set of variables on which two functions agree. -/
+def agreementSet (f g : Var → Var) : Set Var := { x | f x = g x }
+/-- The set of variables on which two functions disagree. -/
+def disagreementSet (f g : Var → Var) : Set Var := { x | f x ≠ g x }
+
+@[simp]
+lemma swap_self {m : Term Var} {x : Var} : m.swap x x = m := by
+  induction m <;> simp_all [swap, permute]
+
+lemma swap_comm {m : Term Var} {x y : Var} : m.swap x y = m.swap y x := by
+  unfold swap
+  rw [Equiv.swap_comm]
+
+@[simp]
+lemma swap_involutive {m : Term Var} {x y : Var} : (m.swap x y).swap x y = m := by
+  induction m <;> simp_all [swap, permute]
+
+@[simp]
+lemma swap_preserves_sizeOf {m : Term Var} {x y : Var} : sizeOf (m.swap x y) = sizeOf m := by
+  induction m <;> simp_all [swap, permute]
+
+@[simp]
+lemma swap_unused {m : Term Var} {x y : Var} : x ∉ m.vars → y ∉ m.vars → m.swap x y = m := by
+  induction m <;> grind [swap, permute, vars]
+
+/-- When `y ∉ m.vars`, `swap x y` and `rename x y` coincide.
+
+This is because `rename x y` only changes `x` to `y` (not `y` to `x`), and when `y` does
+not occur in `m`, swapping and renaming produce the same result. -/
+lemma swap_eq_rename_of_not_mem_vars {m : Term Var} {x y : Var}
+    (hy : y ∉ m.vars) : m.swap x y = m.rename x y := by
+  induction m with
+  | var z =>
+    unfold swap rename
+    grind [Term.vars, permute]
+  | abs z m ih =>
+    simp_all [Term.swap, Term.rename, Term.vars, permute]
+    grind
+  | app n1 n2 ih1 ih2 =>
+    simp_all [Term.swap, Term.rename, Term.vars, permute]
+
+/-- The set of free variables after a swap. -/
+lemma swap_fv {m : Term Var} {x y : Var} :
+    (m.swap x y).fv = m.fv.image fun z => if z = x then y else if z = y then x else z := by
+  induction m with
+  | var z => aesop
+  | abs z m ih =>
+    simp_all [Term.swap, Term.fv, Finset.ext_iff, Finset.mem_image, Finset.mem_sdiff, permute]
+    grind
+  | app m n ih1 ih2 =>
+    simp_all only [Term.swap, Term.fv, permute]
+    rw [Finset.image_union]
+
+/-- Swapping preserves non-membership in `fv`. -/
+lemma fresh_swap {m : Term Var} {x y z : Var} (hzx : z ≠ x) (hzy : z ≠ y) (hzm : z ∉ m.fv) :
+    z ∉ (m.swap x y).fv := by
+  rw [swap_fv]
+  grind
+
+/-- The set of vars after a swap. -/
+lemma swap_vars {m : Term Var} {x y z : Var} (hzm : z ∉ m.vars) :
+    (m.swap x y).vars = m.vars.image fun z => if z = x then y else if z = y then x else z := by
+  induction m with
+  | var w => aesop
+  | abs w m ih =>
+    simp_all [Term.swap, Term.vars, permute]
+    grind
+  | app m n ih1 ih2 =>
+    simp_all only [Term.swap, Term.vars, Finset.image_union, permute]
+    grind
+
+/-- Swapping preserves non-membership in `vars`. -/
+lemma not_mem_vars_swap {m : Term Var} {x y z : Var}
+    (hzx : z ≠ x) (hzy : z ≠ y) (hzm : z ∉ m.vars) : z ∉ (m.swap x y).vars := by
+  rw [swap_vars hzm]
+  grind
+
+/-- `swap` and `rename` commute (modulo the permutation action on the variable arguments). -/
+lemma swap_rename_comm {m : Term Var} {u v x y : Var} :
+    (m.swap u v).rename (Equiv.swap u v x) (Equiv.swap u v y) = (m.rename x y).swap u v := by
+  induction m with
+  | var z =>
+    simp_all [Term.swap, Term.rename, permute]
+    grind
+  | abs z m ih =>
+    simp_all [Term.swap, Term.rename, permute]
+    grind
+  | app m n ih1 ih2 =>
+    simp_all [Term.swap, Term.rename, permute]
+
+lemma swap_rename_comm' {m : Term Var} {u v x z : Var} (hzu : z ≠ u) (hzv : z ≠ v) :
+    (m.swap u v).rename (Equiv.swap u v x) z = (m.rename x z).swap u v := by
+  rw [← @swap_rename_comm _ _ m u v x z]
+  congr 1
+  exact Eq.symm (Equiv.swap_apply_of_ne_of_ne hzu hzv)
+
+lemma swap_comp_eq_of_not_mem_vars {m : Term Var} {a u z : Var}
+    (hu : u ∉ m.vars) (hz : z ∉ m.vars) :
+    (m.swap u a).swap z u = m.swap z a := by
+  induction m with
+  | var x =>
+    simp_all [Term.swap, Term.vars, permute]
+    grind
+  | abs x m ih =>
+    simp_all [Term.swap, Term.vars, permute]
+    grind
+  | app m n m_ih n_ih => simp_all [Term.swap, Term.vars, permute]
+
+/-- Term-level conjugation identity: `(m.swap u v).swap v a = (m.swap u a).swap u v`
+when `a ∉ {u, v}`.
+
+Unlike `swap_comp_eq_of_not_mem_vars`, this holds unconditionally (no freshness needed). -/
+lemma swap_comp_eq_of_ne {m : Term Var} {a u v : Var} (hau : a ≠ u) (hav : a ≠ v) :
+    (m.swap u v).swap v a = (m.swap u a).swap u v := by
+  induction m with
+  | var x => simp_all [Term.swap, permute]; grind
+  | app m n ihm ihn => simp_all [Term.swap, permute]
+  | abs x m ih => simp_all [Term.swap, permute]; grind
+
+/-- If `u` is not among `m`'s variables, then `v` cannot appear in `m.swap u v`
+(the only way `v` could show up is as the image of `u`). -/
+lemma not_mem_swap_target {m : Term Var} {u v : Var} (hu : u ∉ m.vars) : v ∉ (m.swap u v).vars := by
+  rw [swap_vars hu]
+  intro h
+  apply Finset.mem_image.mp at h
+  obtain ⟨a, ham, hau⟩ := h
+  have hau_ne : a ≠ u := by grind
+  by_cases h : a = v
+  · grind
+  · grind
+
+/-- Permuting a term transports its free variables pointwise. -/
+lemma permute_fv (m : Term Var) (π : Equiv.Perm Var) :
+    (m.permute π).fv = m.fv.image π := by
+  induction m with
+  | var x => simp [permute, fv]
+  | app m n ihm ihn => simp [permute, fv, ihm, ihn, Finset.image_union]
+  | abs x m ih =>
+    simp only [permute, fv, ih]
+    rw [Finset.image_sdiff _ _ π.injective]
+    simp
+
+omit [DecidableEq Var] in
+/-- Permuting successively by `π` and `π'` is permutation by their composition. -/
+lemma permute_trans (m : Term Var) (π π' : Equiv.Perm Var) :
+    (m.permute π).permute π' = m.permute (π.trans π') := by
+  induction m <;> simp_all [permute]
+
+/-- A transposition acts on terms in the same way as `Term.swap`. -/
+lemma permute_swap (m : Term Var) (x y : Var) : m.permute (Equiv.swap x y) = m.swap x y := by
+  induction m <;> simp_all [permute, swap, Equiv.swap_apply_def]
+
+-- First 4 case examination of example 1
+lemma desired_condition_cases_z_ne_u_or_v {E E' : Term Var} {a b u v z : Var}
+    (hm1 : z ∉ E.vars ∪ E'.vars ∪ {a, b})
+    (h2 : ((E.rename a z).swap u v) =α ((E'.rename b z).swap u v))
+    (hzu : z ≠ u)
+    (hzv : z ≠ v)
+    : ((E.swap u v).swap (Equiv.swap u v a) z) =α ((E'.swap u v).swap (Equiv.swap u v b) z) := by
+  have hzb : z ≠ b := by simp_all
+  have hza : z ≠ a := by simp_all
+  have z_h1 : z ∉ (E.swap u v).vars := by exact not_mem_vars_swap hzu hzv (by simp_all)
+  have z_h2 : z ∉ (E'.swap u v).vars := by exact not_mem_vars_swap hzu hzv (by simp_all)
+  rw [swap_eq_rename_of_not_mem_vars z_h1]
+  rw [swap_eq_rename_of_not_mem_vars z_h2]
+  rw [← swap_rename_comm' (by grind) (by grind)] at h2
+  rw [← swap_rename_comm' (by grind) (by grind)] at h2
+  have ha : a = u ∨ a = v ∨ (a ≠ u ∧ a ≠ v) := by grind
+  have hb : b = u ∨ b = v ∨ (b ≠ u ∧ b ≠ v) := by grind
+  rcases ha with h' | h' | ⟨hau, hav⟩
+  · rcases hb with h'' | h'' | ⟨hbu, hbv⟩ <;> simp_all
+  · rcases hb with h'' | h'' | ⟨hbu, hbv⟩ <;> simp_all
+  · rcases hb with h'' | h'' | ⟨hbu, hbv⟩ <;> simp_all
+
+-- example 1: use z as witness
+lemma alphaEquiv_swap_preserve_abs_fresh {E E' : Term Var} {a b u v z : Var}
+    (hm : z ∉ E.vars ∪ E'.vars ∪ {a, b})
+    (hbody : ((E.rename a z).swap u v) =α ((E'.rename b z).swap u v))
+    (hzu : z ≠ u) (hzv : z ≠ v) :
+    ((Term.abs a E).swap u v) =α ((Term.abs b E').swap u v) := by
+  have hzE : z ∉ (E.swap u v).vars := not_mem_vars_swap hzu hzv (by simp_all)
+  have hzE' : z ∉ (E'.swap u v).vars := not_mem_vars_swap hzu hzv (by simp_all)
+  have hren := desired_condition_cases_z_ne_u_or_v hm hbody hzu hzv
+  rw [swap_eq_rename_of_not_mem_vars hzE, swap_eq_rename_of_not_mem_vars hzE'] at hren
+  simp only [Term.swap]
+  apply AlphaEquiv.abs (y := z)
+  · simp_all [Finset.mem_union, Finset.mem_insert, swap]
+    grind
+  · exact hren
+
+-- example 2: use v as witness
+lemma alphaEquiv_swap_preserve_abs_fresh_z_eq_u {E E' : Term Var} {a b u v : Var}
+    (hm : u ∉ E.vars ∪ E'.vars ∪ {a, b})
+    (hbody : ((E.rename a u).swap u v) =α ((E'.rename b u).swap u v))
+    (hau : a ≠ u) (hav : a ≠ v) (hbu : b ≠ u) (hbv : b ≠ v) :
+    ((Term.abs a E).swap u v) =α ((Term.abs b E').swap u v) := by
+  have huE : u ∉ E.vars := by simp_all
+  have huE' : u ∉ E'.vars := by simp_all
+  rw [← swap_eq_rename_of_not_mem_vars huE, ← swap_eq_rename_of_not_mem_vars huE'] at hbody
+  rw [swap_comm (m := E) (x := a) (y := u), swap_comm (m := E') (x := b) (y := u)] at hbody
+  rw [← swap_comp_eq_of_ne hau hav, ← swap_comp_eq_of_ne hbu hbv] at hbody
+  rw [swap_comm (m := E.swap u v) (x := v) (y := a)] at hbody
+  rw [swap_comm (m := E'.swap u v) (x := v) (y := b)] at hbody
+  have hvE : v ∉ (E.swap u v).vars := not_mem_swap_target huE
+  have hvE' : v ∉ (E'.swap u v).vars := not_mem_swap_target huE'
+  rw [swap_eq_rename_of_not_mem_vars hvE, swap_eq_rename_of_not_mem_vars hvE'] at hbody
+  apply AlphaEquiv.abs (y := v) <;> (simp_all [swap]; grind)
+
+-- example 3
+lemma alphaEquiv_swap_preserve_abs_b_eq_u {E E' : Term Var} {a u v : Var}
+    (hm : v ∉ E.vars ∪ E'.vars ∪ {a})
+    (hbody : ((E.rename a v).swap u v) =α ((E'.rename u v).swap u v))
+    (hau : a ≠ u) (hav : a ≠ v) (huv : u ≠ v) :
+    ((Term.abs a E).swap u v) =α ((Term.abs u E').swap u v) := by
+  have hvE : v ∉ E.vars := by simp_all
+  have hvE' : v ∉ E'.vars := by simp_all
+  have huE : u ∉ (E.swap u v).vars := by rw [swap_comm]; exact not_mem_swap_target hvE
+  have huE' : u ∉ (E'.swap u v).vars := by rw [swap_comm]; exact not_mem_swap_target hvE'
+  have hL : (E.swap u v).rename a u = (E.rename a v).swap u v := by
+    have h := @swap_rename_comm _ _ E u v a v
+    simp_all
+    grind
+  have hR : (E'.swap u v).rename v u = (E'.rename u v).swap u v := by
+    have h := @swap_rename_comm _ _ E' u v u v
+    simp_all
+  have hbody' : ((E.swap u v).rename a u) =α ((E'.swap u v).rename v u) := by
+    rw [hL, hR]
+    exact hbody
+  apply AlphaEquiv.abs (y := u)
+  · simp_all [Finset.mem_union, Finset.mem_insert, swap]
+    grind
+  · simp_all [swap]
+    grind
+
+-- example 4
+lemma alphaEquiv_swap_preserve_abs_a_eq_b_eq_u {E E' : Term Var} {u v : Var}
+    (hm : v ∉ E.vars ∪ E'.vars ∪ {u})
+    (ih : ((E.rename u v).swap u v) =α ((E'.rename u v).swap u v)) (huv : u ≠ v) :
+    ((Term.abs u E).swap u v) =α ((Term.abs u E').swap u v) := by
+  have hvE : v ∉ E.vars := by simp_all
+  have hvE' : v ∉ E'.vars := by simp_all
+  rw [← swap_eq_rename_of_not_mem_vars hvE, ← swap_eq_rename_of_not_mem_vars hvE'] at ih
+  rw [swap_involutive, swap_involutive] at ih
+  -- now have ih : E =α E'
+  have huE : u ∉ (E.swap u v).vars := by
+    have h := not_mem_swap_target (u := v) (v := u) hvE
+    rwa [swap_comm] at h
+  have huE' : u ∉ (E'.swap u v).vars := by
+    have h := not_mem_swap_target (u := v) (v := u) hvE'
+    rw [swap_comm] at h
+    exact h
+  apply AlphaEquiv.abs (y := u)
+  · simp_all [swap]
+  · simp only [Equiv.swap_apply_left]
+    change ((E.swap u v).rename v u) =α ((E'.swap u v).rename v u)
+    rw [← swap_eq_rename_of_not_mem_vars (m := E.swap u v) (x := v) (y := u) huE]
+    rw [← swap_eq_rename_of_not_mem_vars (m := E'.swap u v) (x := v) (y := u) huE']
+    nth_rw 2 [swap_comm]
+    nth_rw 4 [swap_comm]
+    rw [swap_involutive, swap_involutive]
+    exact ih
+
+variable [HasFresh Var]
+
+/-- Lemma 6.1 [Crole2012]: Swap (transposition) preserves α-equivalence. -/
+lemma AlphaEquiv.swap_preserve {m m' : Term Var} {u v : Var} :
+    m =α m' → (m.swap u v) =α (m'.swap u v) := by
+  intro h1
+  by_cases h2 : u = v
+  · simp_all
+  · change u ≠ v at h2
+    induction h1 with
+    | var => apply AlphaEquiv.refl
+    | abs hm1 hm2 ih =>
+      rename_i z a b E E'
+      have z_h1 : z ≠ a := by simp_all
+      have z_h2 : z ≠ b := by simp_all
+      have h3 : a = u ∨ a = v ∨ (a ≠ u ∧ a ≠ v) := by grind
+      have h4 : b = u ∨ b = v ∨ (b ≠ u ∧ b ≠ v) := by grind
+      have h5 : z = u ∨ z = v ∨ (z ≠ u ∧ z ≠ v) := by grind
+      -- we've got 27 cases to consider
+      rcases h3 with ha | ha | ⟨hau, hav⟩
+      · rcases h4 with hb | hb | ⟨hbu, hbv⟩
+        · rcases h5 with hz | hz | ⟨hzu, hzv⟩
+          · simp_all
+          -- representative example 4 case of: a = u; b = u; z = v
+          · subst ha hb hz
+            exact alphaEquiv_swap_preserve_abs_a_eq_b_eq_u (by simp_all) ih h2
+          -- example 1 reuse
+          · exact alphaEquiv_swap_preserve_abs_fresh hm1 ih hzu hzv
+        · rcases h5 with hz | hz | ⟨hzu, hzv⟩
+          · simp_all
+          · simp_all
+          -- example 1 reuse
+          · exact alphaEquiv_swap_preserve_abs_fresh hm1 ih hzu hzv
+        · rcases h5 with hz | hz | ⟨hzu, hzv⟩
+          · simp_all
+          -- example 3 reuse
+          · subst ha hz
+            apply AlphaEquiv.symm
+            exact
+              (alphaEquiv_swap_preserve_abs_b_eq_u (by simp_all) (AlphaEquiv.symm ih) hbu hbv h2)
+          -- example 1 reuse
+          · exact alphaEquiv_swap_preserve_abs_fresh hm1 ih hzu hzv
+      · rcases h4 with hb | hb | ⟨hbu, hbv⟩
+        · rcases h5 with hz | hz | ⟨hzu, hzv⟩
+          · simp_all
+          · simp_all
+          -- example 1 reuse
+          · exact alphaEquiv_swap_preserve_abs_fresh hm1 ih hzu hzv
+        · rcases h5 with hz | hz | ⟨hzu, hzv⟩
+          -- example 4 reuse
+          · subst ha hb hz
+            nth_rw 1 [swap_comm]
+            nth_rw 2 [swap_comm]
+            symm at z_h2
+            nth_rw 1 [swap_comm] at ih
+            nth_rw 2 [swap_comm] at ih
+            apply alphaEquiv_swap_preserve_abs_a_eq_b_eq_u (by simp_all) ih z_h2
+          · simp_all
+          -- example 1 reuse
+          · exact alphaEquiv_swap_preserve_abs_fresh hm1 ih hzu hzv
+        · rcases h5 with hz | hz | ⟨hzu, hzv⟩
+          -- example 3 reuse
+          · subst ha hz
+            nth_rw 1 [swap_comm]
+            nth_rw 2 [swap_comm]
+            apply AlphaEquiv.symm
+            symm at h2
+            apply alphaEquiv_swap_preserve_abs_b_eq_u (by simp_all) _ hbv hbu h2
+            apply AlphaEquiv.symm
+            nth_rw 1 [swap_comm]
+            nth_rw 2 [swap_comm]
+            exact ih
+          · simp_all
+          -- example 1 reuse
+          · exact alphaEquiv_swap_preserve_abs_fresh hm1 ih hzu hzv
+      · rcases h4 with hb | hb | ⟨hbu, hbv⟩
+        · rcases h5 with hz | hz | ⟨hzu, hzv⟩
+          · simp_all
+          -- representative example 3 case of: a ≠ u, v; b = u; z = v
+          · subst hb; subst hz
+            exact alphaEquiv_swap_preserve_abs_b_eq_u (by simp_all) ih hau hav h2
+          -- example 1 reuse
+          · exact alphaEquiv_swap_preserve_abs_fresh hm1 ih hzu hzv
+        · rcases h5 with hz | hz | ⟨hzu, hzv⟩
+          -- example 3 reuse
+          · subst hb hz
+            nth_rw 1 [swap_comm]
+            nth_rw 2 [swap_comm]
+            symm at h2
+            apply alphaEquiv_swap_preserve_abs_b_eq_u (by simp_all) _ hav hau h2
+            nth_rw 1 [swap_comm]
+            nth_rw 2 [swap_comm]
+            exact ih
+          · simp_all
+          -- example 1 reuse
+          · exact alphaEquiv_swap_preserve_abs_fresh hm1 ih hzu hzv
+        · rcases h5 with hz | hz | ⟨hzu, hzv⟩
+          -- representative example 2 case of: a ≠ u, v; b ≠ u, v; z = u
+          -- use z' = v
+          · subst hz
+            exact alphaEquiv_swap_preserve_abs_fresh_z_eq_u hm1 ih hau hav hbu hbv
+          -- example 2 reuse after adjusting via swap commutativity and choosing z' = u
+          · rw [swap_comm (m := Term.abs a E) (x := u) (y := v),
+                swap_comm (m := Term.abs b E') (x := u) (y := v)]
+            subst hz
+            nth_rw 1 [swap_comm] at ih
+            nth_rw 2 [swap_comm] at ih
+            exact alphaEquiv_swap_preserve_abs_fresh_z_eq_u hm1 ih hav hau hbv hbu
+          -- representative example 1 case of: z ≠ u, v
+          -- use z' = z
+          · exact alphaEquiv_swap_preserve_abs_fresh hm1 ih hzu hzv
+    | app hm1 hm2 ih1 ih2 => exact AlphaEquiv.app ih1 ih2
+
+omit [HasFresh Var] in
+/-- **Lemma 6.2 part 1** [Crole2012]. -/
+lemma permute_eq_of_vars_subset_agreementSet (m : Term Var) (π π' : Equiv.Perm Var)
+    (h : (m.vars : Set Var) ⊆ agreementSet π π') :
+    m.permute π = m.permute π' := by
+  induction m with
+  | var x => simp_all [permute, vars, agreementSet, vars]
+  | abs x m ih =>
+    have hx : π x = π' x := h (by simp [vars])
+    have hm : m.permute π = m.permute π' := ih fun y hy => h (by simp [vars, hy])
+    simp [permute, hx, hm]
+  | app m n ihm ihn =>
+    have hm : m.permute π = m.permute π' := ihm fun y hy => h (by simp [vars, hy])
+    have hn : n.permute π = n.permute π' := ihn fun y hy => h (by simp [vars, hy])
+    simp [permute, hm, hn]
+
+/-- **Lemma 6.2 part 2** [Crole2012]. -/
+lemma permute_alphaEquiv_of_fv_subset_agreementSet (m : Term Var) (π π' : Equiv.Perm Var)
+    (h : (m.fv : Set Var) ⊆ agreementSet π π') :
+    (m.permute π) =α (m.permute π') := by
+  induction m generalizing π π' with
+  | var x =>
+    unfold permute
+    have hx : π x = π' x := by
+      unfold agreementSet at h
+      apply h
+      unfold fv
+      rw [Finset.coe_singleton, Set.mem_singleton_iff]
+    rw [hx]
+    exact AlphaEquiv.var
+  | app m n ihm ihn =>
+    have hm : (m.permute π) =α (m.permute π') := by
+      apply ihm
+      intro x hx
+      apply h
+      unfold fv
+      simp_all
+    have hn : (n.permute π) =α (n.permute π') := by
+      apply ihn
+      intro x hx
+      apply h
+      unfold fv
+      simp_all
+    apply AlphaEquiv.app hm hn
+  | abs a m ih =>
+    let z := HasFresh.fresh ((m.permute π).vars ∪ (m.permute π').vars ∪ {π a, π' a})
+    have hz := HasFresh.fresh_notMem ((m.permute π).vars ∪ (m.permute π').vars ∪ {π a, π' a})
+    have hzπ : z ∉ (m.permute π).vars := by simp_all [z]
+    have hzπ' : z ∉ (m.permute π').vars := by simp_all [z]
+    have hbody :
+      (m.permute (π.trans (Equiv.swap (π a) z))) =α (m.permute (π'.trans (Equiv.swap (π' a) z)))
+      := by
+        apply ih
+        intro x hx
+        simp only [agreementSet, Set.mem_ofPred_eq, Equiv.trans_apply]
+        by_cases hxa : x = a
+        · simp_all
+        · have hagree : π x = π' x := h (by simp [fv, hx, hxa])
+          have hπxa : π x ≠ π a := fun he => hxa (π.injective he)
+          have hπ'xa : π' x ≠ π' a := fun he => hxa (π'.injective he)
+          have hπ'xπa : π' x ≠ π a := by simp_all
+          have hπxz : π x ≠ z := by
+            intro he
+            apply hzπ
+            rw [← he, vars_either_fv_or_bv]
+            apply Finset.mem_union_left
+            rw [permute_fv]
+            exact Finset.mem_image.mpr ⟨x, hx, rfl⟩
+          have hπ'xz : π' x ≠ z := by simp_all
+          simp [Equiv.swap_apply_def, hπ'xa, hπ'xπa, hπ'xz, hagree]
+    rw [← permute_trans, ← permute_trans, permute_swap, permute_swap] at hbody
+    rw [swap_eq_rename_of_not_mem_vars hzπ, swap_eq_rename_of_not_mem_vars hzπ'] at hbody
+    unfold permute
+    apply AlphaEquiv.abs (y := z) (by simp_all [z]) hbody
+
+/-- **Lemma 6.2 part 2** [Crole2012] (specialized). -/
+lemma swap_comp_alphaEquiv_of_not_mem_fv {m : Term Var} {a u z : Var}
+    (hu : u ∉ m.fv) (hz : z ∉ m.fv) :
+    ((m.swap u a).swap z u) =α (m.swap z a) := by
+  let π := (Equiv.swap u a).trans (Equiv.swap z u)
+  let π' := Equiv.swap z a
+  have h : (m.fv : Set Var) ⊆ agreementSet π π' := by
+    intro x hx
+    unfold agreementSet
+    rw [Set.mem_ofPred_eq]
+    grind
+  have h' := permute_alphaEquiv_of_fv_subset_agreementSet m π π' h
+  rw [← permute_trans, permute_swap, permute_swap, permute_swap] at h'
+  exact h'
+
+end LambdaCalculus.Named.Untyped.Term
+
+end Cslib
diff --git a/CslibTests/LambdaCalculus.lean b/CslibTests/LambdaCalculus.lean
index 331516694..372d14fb9 100644
--- a/CslibTests/LambdaCalculus.lean
+++ b/CslibTests/LambdaCalculus.lean
@@ -5,7 +5,8 @@ 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.RenameProperties
+import Cslib.Languages.LambdaCalculus.Named.Untyped.AlphaEquivProperties
 
 /-! # λ-calculus
 
diff --git a/references.bib b/references.bib
index d2a7dfb13..377a455ac 100644
--- a/references.bib
+++ b/references.bib
@@ -551,3 +551,80 @@ @book{Papadimitriou94
   publisher={Addison-Wesley},
   address={Reading, Massachusetts}
 }
+
+@article{Crole2012,
+  title={Alpha equivalence equalities},
+  journal={Theoretical Computer Science},
+  volume={433},
+  pages={1-19},
+  year={2012},
+  issn={0304-3975},
+  doi={https://doi.org/10.1016/j.tcs.2012.01.030},
+  url={https://www.sciencedirect.com/science/article/pii/S0304397512000667},
+  author={Roy L. Crole},
+  keywords={-equivalence, Atom, Context, -expression, Permutation action, Renaming, Variable binding},
+  abstract={Programming languages and logics, which are pervasive in Computer Science, have syntax which involves variable binding constructors. As such, reasoning about such languages in general, and formal reasoning in particular (such as within a theorem prover), requires frameworks within which the syntax may be properly represented. One key requirement is a correct representation of α-equivalence. The current literature provides a number of different definitions of the notion of α-equivalence. The formal definitions may be nameless as in the approach of de Bruijn, or have explicit names, as in the approaches that use either a renaming/substitution axiom, or instead use a notion of variable swapping. The first contribution of this paper is to draw together five definitions of α-equivalence relations and to prove formally and in detail, but using mathematics, that the relations are all equal. There are two key reasons for doing this: Firstly, the literature has many examples of proofs of results involving α-equivalence which contain technical errors. Such examples concern both the application of α-equivalence, and the meta-theory of α-equivalence itself. Secondly, the literature does not currently contain detailed presentations of such results. The point of giving the detail is partly to avoid falling into common error-traps, but mainly to provide clear mathematical machinery that will be useful to those working in the area. This includes systems of inductive rules and proofs by induction, and clear accounts of the key lemmas that support the main proofs. The second contribution is to provide two definitions of α-equivalence relations over (program) contexts, namely expressions with a single meta-variable (or “hole”). One of the definitions is already in the literature, and the other is new. We prove some basic properties of α-equivalence on contexts, and show that the two definitions give rise to the same relation.}
+}
+
+@InProceedings{Gabbay1999,
+  author={Murdoch Gabbay and Andrew Pitts},
+  title={A New Approach to Abstract Syntax Involving Binders},
+  booktitle={Proceedings of the Fourteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1999},
+  year=1999,
+  editor={Giuseppe Longo},
+  month={July}, 
+  pages={214--224},
+  location={Trento, Italy}, 
+  publisher={IEEE Computer Society Press}
+}
+
+@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}
+}
+
+@book{Barendregt1985,
+  author={Hendrik Pieter Barendregt},
+  title={The lambda calculus - its syntax and semantics},
+  series={Studies in logic and the foundations of mathematics},
+  volume={103},
+  publisher={North-Holland},
+  year={1985},
+  isbn={978-0-444-86748-3},
+  timestamp={Fri, 28 Jun 2019 12:45:52 +0200},
+  biburl={https://dblp.org/rec/books/daglib/0067558.bib},
+  bibsource={dblp computer science bibliography, https://dblp.org}
+}
+
+@book{Church1941,
+  ISBN={9780691083940},
+  author={ALONZO CHURCH},
+  publisher={Princeton University Press},
+  title={The Calculi of Lambda Conversion. (AM-6)},
+  year={1941}
+}
+
+@book{Hindley1988,
+  title={Introduction to Combinators and $\lambda$-Calculus},
+  author={Hindley, J. Roger and Seldin, Jonathan P.},
+  series={London Mathematical Society Student Texts},
+  volume={1},
+  year={1988},
+  publisher={Cambridge University Press},
+  address={Cambridge, UK}
+}