From 70543ce0cf38620b5c76929b7541132e907f32e8 Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Tue, 23 Jun 2026 15:48:11 -0600
Subject: [PATCH 01/17] add basic properties

---
 .../LocallyNameless/Untyped/CallByName.lean   | 32 +++++++++++++++++--
 1 file changed, 29 insertions(+), 3 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean
index 7250ae7bb..5792c1cfd 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean
@@ -31,18 +31,44 @@ inductive CBN : Term Var → Term Var → Prop
 /-- Evaluates the leftmost term. -/
 | app : LC Z → CBN M N → CBN (app M Z) (app N Z)
 
-variable {M N : Term Var}
+variable {M M' N N' : Term Var}
 
-/-- The left side of a CBN reduction step is locally closed. -/
+/-- The left side of a Call-by-Name step is locally closed. -/
 lemma CBN.lc_l (step : M ⭢ₙ N) : LC M := by
   induction step with grind
 
+/-- A single Call-by-Name step is a full β-reduction. -/
+lemma CBN.step_to_redex (step : M ⭢ₙ N) : M ↠βᶠ N := by
+  induction step <;> grind [FullBeta.redex_app_l_cong, Relation.ReflTransGen.single]
+
+/-- Call-by-Name reduction is contained in full β-reduction. -/
+lemma CBN.to_redex (step : M ↠ₙ N) : M ↠βᶠ N := by
+  induction step <;> grind [CBN.step_to_redex, Relation.ReflTransGen.trans]
+
+/-- Left congruence rule for application in Call-by-Name reduction. -/
+lemma CBN.steps_app_l_cong (step : M ↠ₙ M') (lc_N : LC N) : Term.app M N ↠ₙ Term.app M' N := by
+  induction step <;> grind [CBN.app]
+
 variable [HasFresh Var] [DecidableEq Var]
 
-/-- The right side of a CBN reduction step is locally closed. -/
+/-- The right side of a Call-by-Name step is locally closed. -/
 lemma CBN.lc_r (step : M ⭢ₙ N) : LC N := by
   induction step with grind
 
+/-- The right side of a Call-by-Name reduction is locally closed. -/
+lemma CBN.steps_lc_r (lc_M : LC M) (step : M ↠ₙ N) : LC N := by
+  induction step <;> grind [CBN.lc_r]
+
+/-- Substitution preserves a single Call-by-Name step. -/
+lemma CBN.step_subst (x : Var) (h : M ⭢ₙ M') (lc_N : LC N) :
+    M[x := N] ⭢ₙ M'[x := N] := by
+  induction h <;> grind [Term.subst_open, Term.subst_lc, CBN.base, CBN.app]
+
+/-- Substitution preserves Call-by-Name reduction. -/
+lemma CBN.steps_subst (x : Var) (step : M ↠ₙ M') (lc_N : LC N) :
+    M[x := N] ↠ₙ M'[x := N] := by
+  induction step <;> grind [CBN.step_subst]
+
 end LambdaCalculus.LocallyNameless.Untyped.Term
 
 end Cslib

From 93dfbbb10d06029f58fc1fbe7a745eb5e08528f6 Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Wed, 24 Jun 2026 06:34:13 -0600
Subject: [PATCH 02/17] add standardization theorem

---
 .../Untyped/StandardReduction.lean            | 171 +++++++++++++++++-
 1 file changed, 169 insertions(+), 2 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index 74d253b5c..5ead02906 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -8,7 +8,7 @@ module
 
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.CallByName
 
-/-! # Standard Reduction
+/-! # Standard Reduction and the Standardization Theorem
 
 ## Reference
 
@@ -18,6 +18,8 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.CallByName
 
 @[expose] public section
 
+set_option linter.unusedDecidableInType false
+
 namespace Cslib
 
 universe u
@@ -39,7 +41,7 @@ inductive Standard : Term Var → Term Var → Prop
 /-- Standard reduction of a head redex. -/
 | rdx : LC m → LC n → m ↠ₙ (abs m') → Standard (m' ^ n) p → Standard (app m n) p
 
-variable {M N : Term Var}
+variable {M N P M' N' : Term Var}
 
 /-- The left side of a standard reduction is locally closed. -/
 lemma Standard.lc_l (step : M ⭢ₛ N) : LC M := by
@@ -58,6 +60,171 @@ lemma Standard.lc_r (step : M ⭢ₛ N) : LC N := by
   case abs xs _ ih => exact LC.abs xs _ ih
   all_goals grind
 
+/-- A single Call-by-Name step is a standard reduction. -/
+lemma Standard.of_cbn_step (step : M ⭢ₙ N) (lc_N : LC N) : M ⭢ₛ N := by
+  induction step
+  case base h_beta =>
+    cases h_beta
+    exact rdx (by assumption) (by assumption) .refl (lc_refl _ lc_N)
+  case app L _ _ lc_L _ ih =>
+    exact app (ih (by cases lc_N; assumption)) (lc_refl L lc_L)
+
+/-- A Call-by-Name step followed by a standard reduction is a standard reduction. -/
+lemma Standard.cbn_step_trans (step : M ⭢ₙ P) (std : P ⭢ₛ N) : M ⭢ₛ N := by
+  induction step generalizing N
+  case base h_beta =>
+    cases h_beta
+    exact rdx (by assumption) (by assumption) .refl std
+  case app step_M ih =>
+    cases std with
+    | app std_L' std_M => exact app (ih std_L') std_M
+    | rdx _ lc_Z cbn_m std_body =>
+      exact rdx (CBN.lc_l step_M) lc_Z (.head step_M cbn_m) std_body
+
+/-- A Call-by-Name reduction followed by a standard reduction is a standard reduction. -/
+lemma Standard.cbn_trans (h1 : M ↠ₙ P) (h2 : P ⭢ₛ N) : M ⭢ₛ N := by
+  induction h1 with
+  | refl => exact h2
+  | tail _ h_step ih => exact ih (cbn_step_trans h_step h2)
+
+/-- Call-by-Name reduction is contained in standard reduction. -/
+lemma Standard.of_cbn (step : M ↠ₙ N) (lc_N : LC N) : M ⭢ₛ N :=
+  cbn_trans step (lc_refl N lc_N)
+
+variable [DecidableEq Var] [HasFresh Var]
+
+/-- Standard reduction is preserved by substitution. -/
+lemma Standard.subst (hM : M ⭢ₛ M') (hN : N ⭢ₛ N') (x : Var) (lc_N : LC N) (lc_N' : LC N') :
+    (M [ x := N ]) ⭢ₛ (M' [ x := N' ]) := by
+  induction hM generalizing N N'
+  case fvar =>
+    simp only [Term.subst_fvar]
+    split
+    · exact hN
+    · exact fvar _
+  case app ihL ihM =>
+    rw [Term.subst_app]
+    exact app (ihL hN lc_N lc_N') (ihM hN lc_N lc_N')
+  case abs m m' _ _ ih =>
+    simp only [Term.subst_abs]
+    apply abs <| free_union [fv] Var
+    intro y hy
+    have h_neq : x ≠ y := by aesop
+    rw [← Term.subst_open_var y x N m h_neq lc_N, ← Term.subst_open_var y x N' m' h_neq lc_N']
+    exact ih y (by aesop) hN lc_N lc_N'
+  case rdx n m' _ lc_m lc_n cbn_m std_p ih =>
+    rw [Term.subst_app]
+    have std_p_subst := ih hN lc_N lc_N'
+    rw [Term.subst_open x N n m' lc_N] at std_p_subst
+    exact rdx (Term.subst_lc (x := x) lc_m lc_N) (Term.subst_lc (x := x) lc_n lc_N)
+      (CBN.steps_subst x cbn_m lc_N) std_p_subst
+
+/-- A single full β-step is a standard reduction. -/
+lemma Standard.of_beta_step (step : M ⭢βᶠ N) (lc_M : LC M) : M ⭢ₛ N := by
+  induction step
+  case base h_beta =>
+    cases h_beta
+    exact rdx (by assumption) (by assumption) .refl
+      (lc_refl _ (Term.beta_lc (by assumption) (by assumption)))
+  case appL A B _ _ _ =>
+    have : LC A := by cases lc_M; assumption
+    apply Standard.app <;> grind [lc_refl]
+  case appR A _ _ _ _ =>
+    have : LC A := by cases lc_M; assumption
+    apply Standard.app <;> grind [lc_refl]
+  case abs ih =>
+    apply Standard.abs <| free_union [fv] Var
+    intro x hx
+    exact ih x (by aesop) (Term.beta_lc lc_M (by constructor))
+
+/-- Standard reduction is contained in full β-reduction. -/
+lemma Standard.to_redex (step : M ⭢ₛ N) : M ↠βᶠ N := by
+  induction step
+  case fvar => rfl
+  case app step_L step_M ih_L ih_M =>
+    exact .trans (FullBeta.redex_app_l_cong ih_L (Standard.lc_l step_M))
+      (FullBeta.redex_app_r_cong ih_M (Standard.lc_r step_L))
+  case abs xs _ ih => exact FullBeta.redex_abs_cong xs ih
+  case rdx n m' _ lc_m lc_n cbn_m std_p ih =>
+    have step1 := FullBeta.redex_app_l_cong (CBN.to_redex cbn_m) lc_n
+    have step2 : Term.app (Term.abs m') n ↠βᶠ (m' ^ n) :=
+      .single (Xi.base (Beta.beta (CBN.steps_lc_r lc_m cbn_m) lc_n))
+    exact .trans step1 (.trans step2 ih)
+
+/-- If a standard reduction reaches an abstraction, then its leading Call-by-Name
+    reduction reaches an abstraction that standardly reduces to the same target. -/
+lemma Standard.abs_inv (h : M ⭢ₛ N) (M' : Term Var) (eq : N = Term.abs M') :
+    ∃ M'', M ↠ₙ Term.abs M'' ∧ Term.abs M'' ⭢ₛ Term.abs M' := by
+  induction h generalizing M'
+  case fvar => trivial
+  case app => trivial
+  case abs m_body m_target xs h_body ih =>
+    cases eq
+    exact ⟨m_body, .refl, Standard.abs xs h_body⟩
+  case rdx m1 n1 m1' p1 lc_m1 lc_n1 cbn_m1 _ ih =>
+    have ⟨p'', cbn_body, std_p''⟩ := ih M' eq
+    have step1 : Term.app m1 n1 ↠ₙ Term.app (Term.abs m1') n1 := CBN.steps_app_l_cong cbn_m1 lc_n1
+    have step2 : Term.app (Term.abs m1') n1 ⭢ₙ (m1' ^ n1) :=
+      CBN.base (Beta.beta (CBN.steps_lc_r lc_m1 cbn_m1) lc_n1)
+    exact ⟨p'', .trans step1 (.head step2 cbn_body), std_p''⟩
+
+/-- Standard reduction of abstractions is preserved by opening. -/
+lemma Standard.abs_subst
+    (h_abs : Term.abs M ⭢ₛ Term.abs M') (hN : N ⭢ₛ N') (lc_N : LC N) (lc_N' : LC N') :
+    (M ^ N) ⭢ₛ (M' ^ N') := by
+  cases h_abs
+  case abs h_body =>
+    have ⟨y, _⟩ := fresh_exists <| free_union [fv] Var
+    have h_subst := Standard.subst (h_body y (by aesop)) hN y lc_N lc_N'
+    rw [← Term.subst_intro y N M (by aesop), ← Term.subst_intro y N' M' (by aesop)] at h_subst
+    exact h_subst
+
+/-- A standard reduction followed by a full β-step is a standard reduction. -/
+lemma Standard.trans_step (h1 : M ⭢ₛ P) (h2 : P ⭢βᶠ N) : M ⭢ₛ N := by
+  induction h1 generalizing N
+  case fvar => contradiction
+  case rdx lc_L lc_M cbn _ ih => exact Standard.rdx lc_L lc_M cbn (ih h2)
+  case abs p_body ih =>
+    cases h2
+    case abs ih_beta =>
+      apply Standard.abs <| free_union [fv] Var
+      intro y hy
+      exact ih y (by aesop) (ih_beta y (by aesop))
+    · grind
+  case app L1 _ M1 _ std_L std_M ih_L ih_M =>
+    cases h2
+    case appL step_M => exact Standard.app std_L (ih_M step_M)
+    case appR step_L _ => exact Standard.app (ih_L step_L) std_M
+    case base h_beta =>
+      cases h_beta
+      have ⟨L1', cbn_L1, std_abs⟩ := Standard.abs_inv std_L _ rfl
+      have std_subst := Standard.abs_subst std_abs std_M (Standard.lc_l std_M) (Standard.lc_r std_M)
+      have step1 : Term.app L1 M1 ↠ₙ Term.app (Term.abs L1') M1 :=
+        CBN.steps_app_l_cong cbn_L1 (Standard.lc_l std_M)
+      have step2 : Term.app (Term.abs L1') M1 ⭢ₙ (L1' ^ M1) :=
+        CBN.base (Beta.beta (CBN.steps_lc_r (Standard.lc_l std_L) cbn_L1) (Standard.lc_l std_M))
+      exact Standard.cbn_trans (.trans step1 (.single step2)) std_subst
+
+/-- A standard reduction followed by a full β-reduction is a standard reduction. -/
+lemma Standard.trans_redex (h1 : M ⭢ₛ P) (h2 : P ↠βᶠ N) : M ⭢ₛ N := by
+  induction h2 with
+  | refl => exact h1
+  | tail _ step ih => exact Standard.trans_step ih step
+
+/-- Standard reduction is transitive. -/
+lemma Standard.trans (h1 : M ⭢ₛ P) (h2 : P ⭢ₛ N) : M ⭢ₛ N :=
+  trans_redex h1 (to_redex h2)
+
+/-- The standardization theorem: every full β-reduction is a standard reduction. -/
+theorem Standard.standardization (lc_M : LC M) (step : M ↠βᶠ N) : M ⭢ₛ N := by
+  induction step with
+  | refl => exact Standard.lc_refl M lc_M
+  | tail _ h_step ih => exact ih.trans (Standard.of_beta_step h_step (FullBeta.step_lc_l h_step))
+
+/-- Standard reduction coincides with full β-reduction on locally closed terms. -/
+theorem Standard.iff_redex (lc_M : LC M) : M ⭢ₛ N ↔ M ↠βᶠ N :=
+  ⟨to_redex, standardization lc_M⟩
+
 end LambdaCalculus.LocallyNameless.Untyped.Term
 
 end Cslib

From 58eca136679d9398b0cf29a6cfa12679ab07ec60 Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Tue, 7 Jul 2026 13:05:29 -0600
Subject: [PATCH 03/17] fix notation

---
 .../LocallyNameless/Untyped/StandardReduction.lean              | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index 5ead02906..e29d6f901 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -95,7 +95,7 @@ variable [DecidableEq Var] [HasFresh Var]
 
 /-- Standard reduction is preserved by substitution. -/
 lemma Standard.subst (hM : M ⭢ₛ M') (hN : N ⭢ₛ N') (x : Var) (lc_N : LC N) (lc_N' : LC N') :
-    (M [ x := N ]) ⭢ₛ (M' [ x := N' ]) := by
+    (M[x := N]) ⭢ₛ (M'[x := N']) := by
   induction hM generalizing N N'
   case fvar =>
     simp only [Term.subst_fvar]

From 668a47f32305a4bb24a5a8d9c90d42a43015aad9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maximiliano=20Onofre=20Mart=C3=ADnez?=
 <maxonomar@ciencias.unam.mx>
Date: Wed, 8 Jul 2026 12:09:45 -0600
Subject: [PATCH 04/17] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 .../LocallyNameless/Untyped/StandardReduction.lean             | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index e29d6f901..5cffa3b76 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -127,8 +127,7 @@ lemma Standard.of_beta_step (step : M ⭢βᶠ N) (lc_M : LC M) : M ⭢ₛ N :=
     exact rdx (by assumption) (by assumption) .refl
       (lc_refl _ (Term.beta_lc (by assumption) (by assumption)))
   case appL A B _ _ _ =>
-    have : LC A := by cases lc_M; assumption
-    apply Standard.app <;> grind [lc_refl]
+    apply Standard.app <;> grind [cases LC, lc_refl]
   case appR A _ _ _ _ =>
     have : LC A := by cases lc_M; assumption
     apply Standard.app <;> grind [lc_refl]

From 2b89df839d51d4ce4265dbf82cd6e6d0aa2f972f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maximiliano=20Onofre=20Mart=C3=ADnez?=
 <maxonomar@ciencias.unam.mx>
Date: Wed, 8 Jul 2026 12:10:02 -0600
Subject: [PATCH 05/17] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 .../LocallyNameless/Untyped/StandardReduction.lean              | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index 5cffa3b76..069e2fefe 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -188,7 +188,7 @@ lemma Standard.trans_step (h1 : M ⭢ₛ P) (h2 : P ⭢βᶠ N) : M ⭢ₛ N :=
     case abs ih_beta =>
       apply Standard.abs <| free_union [fv] Var
       intro y hy
-      exact ih y (by aesop) (ih_beta y (by aesop))
+      exact ih y (by grind) (ih_beta y (by grind))
     · grind
   case app L1 _ M1 _ std_L std_M ih_L ih_M =>
     cases h2

From a9ced4ff7df179f2d8b471e796148a7f9e0c1a88 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maximiliano=20Onofre=20Mart=C3=ADnez?=
 <maxonomar@ciencias.unam.mx>
Date: Wed, 8 Jul 2026 12:10:15 -0600
Subject: [PATCH 06/17] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 .../LocallyNameless/Untyped/StandardReduction.lean            | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index 069e2fefe..ec1f55fd7 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -174,8 +174,8 @@ lemma Standard.abs_subst
   cases h_abs
   case abs h_body =>
     have ⟨y, _⟩ := fresh_exists <| free_union [fv] Var
-    have h_subst := Standard.subst (h_body y (by aesop)) hN y lc_N lc_N'
-    rw [← Term.subst_intro y N M (by aesop), ← Term.subst_intro y N' M' (by aesop)] at h_subst
+    have h_subst := Standard.subst (h_body y (by grind)) hN y lc_N lc_N'
+    rw [← Term.subst_intro y N M (by grind), ← Term.subst_intro y N' M' (by grind)] at h_subst
     exact h_subst
 
 /-- A standard reduction followed by a full β-step is a standard reduction. -/

From 94f34777f3c06ad83b52c7c95846df068c2c17b3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maximiliano=20Onofre=20Mart=C3=ADnez?=
 <maxonomar@ciencias.unam.mx>
Date: Wed, 8 Jul 2026 12:10:38 -0600
Subject: [PATCH 07/17] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 .../LocallyNameless/Untyped/StandardReduction.lean              | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index ec1f55fd7..8d81d5494 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -134,7 +134,7 @@ lemma Standard.of_beta_step (step : M ⭢βᶠ N) (lc_M : LC M) : M ⭢ₛ N :=
   case abs ih =>
     apply Standard.abs <| free_union [fv] Var
     intro x hx
-    exact ih x (by aesop) (Term.beta_lc lc_M (by constructor))
+    exact ih x (by grind) (Term.beta_lc lc_M (by constructor))
 
 /-- Standard reduction is contained in full β-reduction. -/
 lemma Standard.to_redex (step : M ⭢ₛ N) : M ↠βᶠ N := by

From d21d9da90f01c877b7ac1fd67fe6f56ca1afa6f4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maximiliano=20Onofre=20Mart=C3=ADnez?=
 <maxonomar@ciencias.unam.mx>
Date: Wed, 8 Jul 2026 12:11:22 -0600
Subject: [PATCH 08/17] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 .../LocallyNameless/Untyped/StandardReduction.lean            | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index 8d81d5494..d53e5d891 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -109,9 +109,9 @@ lemma Standard.subst (hM : M ⭢ₛ M') (hN : N ⭢ₛ N') (x : Var) (lc_N : LC
     simp only [Term.subst_abs]
     apply abs <| free_union [fv] Var
     intro y hy
-    have h_neq : x ≠ y := by aesop
+    have h_neq : x ≠ y := by grind
     rw [← Term.subst_open_var y x N m h_neq lc_N, ← Term.subst_open_var y x N' m' h_neq lc_N']
-    exact ih y (by aesop) hN lc_N lc_N'
+    exact ih y (by grind) hN lc_N lc_N'
   case rdx n m' _ lc_m lc_n cbn_m std_p ih =>
     rw [Term.subst_app]
     have std_p_subst := ih hN lc_N lc_N'

From a2a5b28801691c56335d6e15fcadb07ccc272bc6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maximiliano=20Onofre=20Mart=C3=ADnez?=
 <maxonomar@ciencias.unam.mx>
Date: Wed, 8 Jul 2026 12:13:15 -0600
Subject: [PATCH 09/17] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 .../LocallyNameless/Untyped/StandardReduction.lean             | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index d53e5d891..aec230181 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -78,8 +78,7 @@ lemma Standard.cbn_step_trans (step : M ⭢ₙ P) (std : P ⭢ₛ N) : M ⭢ₛ
   case app step_M ih =>
     cases std with
     | app std_L' std_M => exact app (ih std_L') std_M
-    | rdx _ lc_Z cbn_m std_body =>
-      exact rdx (CBN.lc_l step_M) lc_Z (.head step_M cbn_m) std_body
+    | rdx _ lc_Z cbn_m std_body => exact rdx (CBN.lc_l step_M) lc_Z (.head step_M cbn_m) std_body
 
 /-- A Call-by-Name reduction followed by a standard reduction is a standard reduction. -/
 lemma Standard.cbn_trans (h1 : M ↠ₙ P) (h2 : P ⭢ₛ N) : M ⭢ₛ N := by

From 7b433629a878e19fafa2c5c11ed0f2e82637fc03 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maximiliano=20Onofre=20Mart=C3=ADnez?=
 <maxonomar@ciencias.unam.mx>
Date: Wed, 8 Jul 2026 12:14:46 -0600
Subject: [PATCH 10/17] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 .../LocallyNameless/Untyped/StandardReduction.lean             | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index aec230181..5686a44f6 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -115,8 +115,7 @@ lemma Standard.subst (hM : M ⭢ₛ M') (hN : N ⭢ₛ N') (x : Var) (lc_N : LC
     rw [Term.subst_app]
     have std_p_subst := ih hN lc_N lc_N'
     rw [Term.subst_open x N n m' lc_N] at std_p_subst
-    exact rdx (Term.subst_lc (x := x) lc_m lc_N) (Term.subst_lc (x := x) lc_n lc_N)
-      (CBN.steps_subst x cbn_m lc_N) std_p_subst
+    exact rdx (subst_lc lc_m lc_N) (subst_lc lc_n lc_N) (CBN.steps_subst x cbn_m lc_N) std_p_subst
 
 /-- A single full β-step is a standard reduction. -/
 lemma Standard.of_beta_step (step : M ⭢βᶠ N) (lc_M : LC M) : M ⭢ₛ N := by

From 1399c5f57a1163e83fad262fd19b396e1e914717 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maximiliano=20Onofre=20Mart=C3=ADnez?=
 <maxonomar@ciencias.unam.mx>
Date: Wed, 8 Jul 2026 12:19:17 -0600
Subject: [PATCH 11/17] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 .../LocallyNameless/Untyped/StandardReduction.lean             | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index 5686a44f6..49093a73e 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -67,7 +67,8 @@ lemma Standard.of_cbn_step (step : M ⭢ₙ N) (lc_N : LC N) : M ⭢ₛ N := by
     cases h_beta
     exact rdx (by assumption) (by assumption) .refl (lc_refl _ lc_N)
   case app L _ _ lc_L _ ih =>
-    exact app (ih (by cases lc_N; assumption)) (lc_refl L lc_L)
+    cases lc_N
+    exact app (ih (by assumption)) (lc_refl L lc_L)
 
 /-- A Call-by-Name step followed by a standard reduction is a standard reduction. -/
 lemma Standard.cbn_step_trans (step : M ⭢ₙ P) (std : P ⭢ₛ N) : M ⭢ₛ N := by

From 582d715673b76baaf22f97c14ecab6d14118ba8d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maximiliano=20Onofre=20Mart=C3=ADnez?=
 <maxonomar@ciencias.unam.mx>
Date: Wed, 8 Jul 2026 12:19:26 -0600
Subject: [PATCH 12/17] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 .../LocallyNameless/Untyped/StandardReduction.lean             | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index 49093a73e..79e3b780a 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -145,8 +145,7 @@ lemma Standard.to_redex (step : M ⭢ₛ N) : M ↠βᶠ N := by
   case abs xs _ ih => exact FullBeta.redex_abs_cong xs ih
   case rdx n m' _ lc_m lc_n cbn_m std_p ih =>
     have step1 := FullBeta.redex_app_l_cong (CBN.to_redex cbn_m) lc_n
-    have step2 : Term.app (Term.abs m') n ↠βᶠ (m' ^ n) :=
-      .single (Xi.base (Beta.beta (CBN.steps_lc_r lc_m cbn_m) lc_n))
+    have step2 : m'.abs.app n ↠βᶠ m' ^ n := .single (.base (.beta (CBN.steps_lc_r lc_m cbn_m) lc_n))
     exact .trans step1 (.trans step2 ih)
 
 /-- If a standard reduction reaches an abstraction, then its leading Call-by-Name

From ee31d1d7a0071d974b199bea90e09c7314e034e9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maximiliano=20Onofre=20Mart=C3=ADnez?=
 <maxonomar@ciencias.unam.mx>
Date: Wed, 8 Jul 2026 12:19:40 -0600
Subject: [PATCH 13/17] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 .../LambdaCalculus/LocallyNameless/Untyped/CallByName.lean    | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean
index 5792c1cfd..0c83bb9c3 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean
@@ -39,7 +39,9 @@ lemma CBN.lc_l (step : M ⭢ₙ N) : LC M := by
 
 /-- A single Call-by-Name step is a full β-reduction. -/
 lemma CBN.step_to_redex (step : M ⭢ₙ N) : M ↠βᶠ N := by
-  induction step <;> grind [FullBeta.redex_app_l_cong, Relation.ReflTransGen.single]
+  induction step with
+  · grind [Relation.ReflTransGen.single]
+  · grind [FullBeta.redex_app_l_cong]
 
 /-- Call-by-Name reduction is contained in full β-reduction. -/
 lemma CBN.to_redex (step : M ↠ₙ N) : M ↠βᶠ N := by

From 60c2d5bdd7a91eae0984c6e95e1a6886f791569a Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Wed, 8 Jul 2026 12:34:45 -0600
Subject: [PATCH 14/17] refactor proofs per review feedback

---
 .../LocallyNameless/Untyped/CallByName.lean   |  4 +--
 .../Untyped/StandardReduction.lean            | 31 +++++++++----------
 2 files changed, 17 insertions(+), 18 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean
index 0c83bb9c3..9523f570c 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean
@@ -40,8 +40,8 @@ lemma CBN.lc_l (step : M ⭢ₙ N) : LC M := by
 /-- A single Call-by-Name step is a full β-reduction. -/
 lemma CBN.step_to_redex (step : M ⭢ₙ N) : M ↠βᶠ N := by
   induction step with
-  · grind [Relation.ReflTransGen.single]
-  · grind [FullBeta.redex_app_l_cong]
+  | base h => exact .single (.base h)
+  | app lc_Z _ ih => exact FullBeta.redex_app_l_cong ih lc_Z
 
 /-- Call-by-Name reduction is contained in full β-reduction. -/
 lemma CBN.to_redex (step : M ↠ₙ N) : M ↠βᶠ N := by
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index 79e3b780a..4fa547a35 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -125,11 +125,12 @@ lemma Standard.of_beta_step (step : M ⭢βᶠ N) (lc_M : LC M) : M ⭢ₛ N :=
     cases h_beta
     exact rdx (by assumption) (by assumption) .refl
       (lc_refl _ (Term.beta_lc (by assumption) (by assumption)))
-  case appL A B _ _ _ =>
-    apply Standard.app <;> grind [cases LC, lc_refl]
-  case appR A _ _ _ _ =>
-    have : LC A := by cases lc_M; assumption
-    apply Standard.app <;> grind [lc_refl]
+  case appL Z A B lc_Z _ ih =>
+    cases lc_M
+    exact Standard.app (lc_refl Z lc_Z) (ih (by assumption))
+  case appR Z A B lc_Z _ ih =>
+    cases lc_M
+    exact Standard.app (ih (by assumption)) (lc_refl Z lc_Z)
   case abs ih =>
     apply Standard.abs <| free_union [fv] Var
     intro x hx
@@ -157,12 +158,11 @@ lemma Standard.abs_inv (h : M ⭢ₛ N) (M' : Term Var) (eq : N = Term.abs M') :
   case app => trivial
   case abs m_body m_target xs h_body ih =>
     cases eq
-    exact ⟨m_body, .refl, Standard.abs xs h_body⟩
+    exact ⟨m_body, .refl, .abs xs h_body⟩
   case rdx m1 n1 m1' p1 lc_m1 lc_n1 cbn_m1 _ ih =>
     have ⟨p'', cbn_body, std_p''⟩ := ih M' eq
-    have step1 : Term.app m1 n1 ↠ₙ Term.app (Term.abs m1') n1 := CBN.steps_app_l_cong cbn_m1 lc_n1
-    have step2 : Term.app (Term.abs m1') n1 ⭢ₙ (m1' ^ n1) :=
-      CBN.base (Beta.beta (CBN.steps_lc_r lc_m1 cbn_m1) lc_n1)
+    have step1 : m1.app n1 ↠ₙ m1'.abs.app n1 := CBN.steps_app_l_cong cbn_m1 lc_n1
+    have step2 : m1'.abs.app n1 ⭢ₙ m1' ^ n1 := .base (.beta (CBN.steps_lc_r lc_m1 cbn_m1) lc_n1)
     exact ⟨p'', .trans step1 (.head step2 cbn_body), std_p''⟩
 
 /-- Standard reduction of abstractions is preserved by opening. -/
@@ -180,7 +180,7 @@ lemma Standard.abs_subst
 lemma Standard.trans_step (h1 : M ⭢ₛ P) (h2 : P ⭢βᶠ N) : M ⭢ₛ N := by
   induction h1 generalizing N
   case fvar => contradiction
-  case rdx lc_L lc_M cbn _ ih => exact Standard.rdx lc_L lc_M cbn (ih h2)
+  case rdx lc_L lc_M cbn _ ih => exact .rdx lc_L lc_M cbn (ih h2)
   case abs p_body ih =>
     cases h2
     case abs ih_beta =>
@@ -190,16 +190,15 @@ lemma Standard.trans_step (h1 : M ⭢ₛ P) (h2 : P ⭢βᶠ N) : M ⭢ₛ N :=
     · grind
   case app L1 _ M1 _ std_L std_M ih_L ih_M =>
     cases h2
-    case appL step_M => exact Standard.app std_L (ih_M step_M)
-    case appR step_L _ => exact Standard.app (ih_L step_L) std_M
+    case appL step_M => exact .app std_L (ih_M step_M)
+    case appR step_L _ => exact .app (ih_L step_L) std_M
     case base h_beta =>
       cases h_beta
       have ⟨L1', cbn_L1, std_abs⟩ := Standard.abs_inv std_L _ rfl
       have std_subst := Standard.abs_subst std_abs std_M (Standard.lc_l std_M) (Standard.lc_r std_M)
-      have step1 : Term.app L1 M1 ↠ₙ Term.app (Term.abs L1') M1 :=
-        CBN.steps_app_l_cong cbn_L1 (Standard.lc_l std_M)
-      have step2 : Term.app (Term.abs L1') M1 ⭢ₙ (L1' ^ M1) :=
-        CBN.base (Beta.beta (CBN.steps_lc_r (Standard.lc_l std_L) cbn_L1) (Standard.lc_l std_M))
+      have step1 : L1.app M1 ↠ₙ L1'.abs.app M1 := CBN.steps_app_l_cong cbn_L1 (Standard.lc_l std_M)
+      have step2 : L1'.abs.app M1 ⭢ₙ L1' ^ M1 :=
+        .base (.beta (CBN.steps_lc_r (Standard.lc_l std_L) cbn_L1) (Standard.lc_l std_M))
       exact Standard.cbn_trans (.trans step1 (.single step2)) std_subst
 
 /-- A standard reduction followed by a full β-reduction is a standard reduction. -/

From 31c1f37f4f8c0c9874091b33cbcb1a424c7ce4af Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Wed, 8 Jul 2026 12:48:02 -0600
Subject: [PATCH 15/17] add Trans instances for standard reduction

---
 .../LocallyNameless/Untyped/StandardReduction.lean       | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index 4fa547a35..6f21d3556 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -211,6 +211,15 @@ lemma Standard.trans_redex (h1 : M ⭢ₛ P) (h2 : P ↠βᶠ N) : M ⭢ₛ N :=
 lemma Standard.trans (h1 : M ⭢ₛ P) (h2 : P ⭢ₛ N) : M ⭢ₛ N :=
   trans_redex h1 (to_redex h2)
 
+instance : Trans (· ⭢ₛ · : Term Var → Term Var → Prop) (· ⭢βᶠ ·) (· ⭢ₛ ·) where
+  trans := Standard.trans_step
+
+instance : Trans (· ⭢ₛ · : Term Var → Term Var → Prop) (· ↠βᶠ ·) (· ⭢ₛ ·) where
+  trans := Standard.trans_redex
+
+instance : Trans (· ⭢ₛ · : Term Var → Term Var → Prop) (· ⭢ₛ ·) (· ⭢ₛ ·) where
+  trans := Standard.trans
+
 /-- The standardization theorem: every full β-reduction is a standard reduction. -/
 theorem Standard.standardization (lc_M : LC M) (step : M ↠βᶠ N) : M ⭢ₛ N := by
   induction step with

From 624ddbd4a3fde6da9a777d7ad6114bafd38d03e1 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Thu, 9 Jul 2026 04:55:38 +0100
Subject: [PATCH 16/17] split out branches of grind proofs

---
 .../LocallyNameless/Untyped/CallByName.lean   | 20 ++++++++++++++-----
 1 file changed, 15 insertions(+), 5 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean
index 9523f570c..a2be62e5a 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean
@@ -45,11 +45,15 @@ lemma CBN.step_to_redex (step : M ⭢ₙ N) : M ↠βᶠ N := by
 
 /-- Call-by-Name reduction is contained in full β-reduction. -/
 lemma CBN.to_redex (step : M ↠ₙ N) : M ↠βᶠ N := by
-  induction step <;> grind [CBN.step_to_redex, Relation.ReflTransGen.trans]
+  induction step
+  · rfl
+  · grind [CBN.step_to_redex, Relation.ReflTransGen.trans]
 
 /-- Left congruence rule for application in Call-by-Name reduction. -/
 lemma CBN.steps_app_l_cong (step : M ↠ₙ M') (lc_N : LC N) : Term.app M N ↠ₙ Term.app M' N := by
-  induction step <;> grind [CBN.app]
+  induction step
+  · rfl
+  · grind [CBN.app]
 
 variable [HasFresh Var] [DecidableEq Var]
 
@@ -59,17 +63,23 @@ lemma CBN.lc_r (step : M ⭢ₙ N) : LC N := by
 
 /-- The right side of a Call-by-Name reduction is locally closed. -/
 lemma CBN.steps_lc_r (lc_M : LC M) (step : M ↠ₙ N) : LC N := by
-  induction step <;> grind [CBN.lc_r]
+  induction step
+  · exact lc_M
+  · grind [CBN.lc_r]
 
 /-- Substitution preserves a single Call-by-Name step. -/
 lemma CBN.step_subst (x : Var) (h : M ⭢ₙ M') (lc_N : LC N) :
     M[x := N] ⭢ₙ M'[x := N] := by
-  induction h <;> grind [Term.subst_open, Term.subst_lc, CBN.base, CBN.app]
+  induction h
+  · grind [Term.subst_open, CBN.base]
+  · grind [CBN.app]
 
 /-- Substitution preserves Call-by-Name reduction. -/
 lemma CBN.steps_subst (x : Var) (step : M ↠ₙ M') (lc_N : LC N) :
     M[x := N] ↠ₙ M'[x := N] := by
-  induction step <;> grind [CBN.step_subst]
+  induction step
+  · rfl
+  · grind [CBN.step_subst]
 
 end LambdaCalculus.LocallyNameless.Untyped.Term
 

From c188914886e73b5769542e3e7252af2f38aba345 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Thu, 9 Jul 2026 04:55:53 +0100
Subject: [PATCH 17/17] misc namespace golf

---
 .../Untyped/StandardReduction.lean            | 59 ++++++++-----------
 1 file changed, 23 insertions(+), 36 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index 6f21d3556..e9cfe09ec 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -79,7 +79,7 @@ lemma Standard.cbn_step_trans (step : M ⭢ₙ P) (std : P ⭢ₛ N) : M ⭢ₛ
   case app step_M ih =>
     cases std with
     | app std_L' std_M => exact app (ih std_L') std_M
-    | rdx _ lc_Z cbn_m std_body => exact rdx (CBN.lc_l step_M) lc_Z (.head step_M cbn_m) std_body
+    | rdx _ lc_Z cbn_m std_body => exact rdx step_M.lc_l lc_Z (.head step_M cbn_m) std_body
 
 /-- A Call-by-Name reduction followed by a standard reduction is a standard reduction. -/
 lemma Standard.cbn_trans (h1 : M ↠ₙ P) (h2 : P ⭢ₛ N) : M ⭢ₛ N := by
@@ -102,16 +102,10 @@ lemma Standard.subst (hM : M ⭢ₛ M') (hN : N ⭢ₛ N') (x : Var) (lc_N : LC
     split
     · exact hN
     · exact fvar _
-  case app ihL ihM =>
-    rw [Term.subst_app]
-    exact app (ihL hN lc_N lc_N') (ihM hN lc_N lc_N')
+  case app ihL ihM => exact app (ihL hN lc_N lc_N') (ihM hN lc_N lc_N')
   case abs m m' _ _ ih =>
-    simp only [Term.subst_abs]
     apply abs <| free_union [fv] Var
-    intro y hy
-    have h_neq : x ≠ y := by grind
-    rw [← Term.subst_open_var y x N m h_neq lc_N, ← Term.subst_open_var y x N' m' h_neq lc_N']
-    exact ih y (by grind) hN lc_N lc_N'
+    grind
   case rdx n m' _ lc_m lc_n cbn_m std_p ih =>
     rw [Term.subst_app]
     have std_p_subst := ih hN lc_N lc_N'
@@ -121,31 +115,28 @@ lemma Standard.subst (hM : M ⭢ₛ M') (hN : N ⭢ₛ N') (x : Var) (lc_N : LC
 /-- A single full β-step is a standard reduction. -/
 lemma Standard.of_beta_step (step : M ⭢βᶠ N) (lc_M : LC M) : M ⭢ₛ N := by
   induction step
-  case base h_beta =>
-    cases h_beta
-    exact rdx (by assumption) (by assumption) .refl
-      (lc_refl _ (Term.beta_lc (by assumption) (by assumption)))
+  case base h_beta => grind [rdx, lc_refl]
   case appL Z A B lc_Z _ ih =>
     cases lc_M
-    exact Standard.app (lc_refl Z lc_Z) (ih (by assumption))
+    exact app (lc_refl Z lc_Z) (ih (by assumption))
   case appR Z A B lc_Z _ ih =>
     cases lc_M
-    exact Standard.app (ih (by assumption)) (lc_refl Z lc_Z)
+    exact app (ih (by assumption)) (lc_refl Z lc_Z)
   case abs ih =>
-    apply Standard.abs <| free_union [fv] Var
+    apply abs <| free_union [fv] Var
     intro x hx
     exact ih x (by grind) (Term.beta_lc lc_M (by constructor))
 
+open FullBeta in
 /-- Standard reduction is contained in full β-reduction. -/
 lemma Standard.to_redex (step : M ⭢ₛ N) : M ↠βᶠ N := by
   induction step
   case fvar => rfl
   case app step_L step_M ih_L ih_M =>
-    exact .trans (FullBeta.redex_app_l_cong ih_L (Standard.lc_l step_M))
-      (FullBeta.redex_app_r_cong ih_M (Standard.lc_r step_L))
+    exact .trans (redex_app_l_cong ih_L step_M.lc_l) (redex_app_r_cong ih_M step_L.lc_r)
   case abs xs _ ih => exact FullBeta.redex_abs_cong xs ih
   case rdx n m' _ lc_m lc_n cbn_m std_p ih =>
-    have step1 := FullBeta.redex_app_l_cong (CBN.to_redex cbn_m) lc_n
+    have step1 := redex_app_l_cong (CBN.to_redex cbn_m) lc_n
     have step2 : m'.abs.app n ↠βᶠ m' ^ n := .single (.base (.beta (CBN.steps_lc_r lc_m cbn_m) lc_n))
     exact .trans step1 (.trans step2 ih)
 
@@ -172,9 +163,8 @@ lemma Standard.abs_subst
   cases h_abs
   case abs h_body =>
     have ⟨y, _⟩ := fresh_exists <| free_union [fv] Var
-    have h_subst := Standard.subst (h_body y (by grind)) hN y lc_N lc_N'
-    rw [← Term.subst_intro y N M (by grind), ← Term.subst_intro y N' M' (by grind)] at h_subst
-    exact h_subst
+    have := subst (h_body y (by grind)) hN y lc_N lc_N'
+    grind
 
 /-- A standard reduction followed by a full β-step is a standard reduction. -/
 lemma Standard.trans_step (h1 : M ⭢ₛ P) (h2 : P ⭢βᶠ N) : M ⭢ₛ N := by
@@ -183,29 +173,26 @@ lemma Standard.trans_step (h1 : M ⭢ₛ P) (h2 : P ⭢βᶠ N) : M ⭢ₛ N :=
   case rdx lc_L lc_M cbn _ ih => exact .rdx lc_L lc_M cbn (ih h2)
   case abs p_body ih =>
     cases h2
-    case abs ih_beta =>
-      apply Standard.abs <| free_union [fv] Var
-      intro y hy
-      exact ih y (by grind) (ih_beta y (by grind))
     · grind
-  case app L1 _ M1 _ std_L std_M ih_L ih_M =>
+    · apply abs <| free_union [fv] Var
+      grind
+  case app L' _ M _ std_L std_M ih_L ih_M =>
     cases h2
     case appL step_M => exact .app std_L (ih_M step_M)
     case appR step_L _ => exact .app (ih_L step_L) std_M
     case base h_beta =>
       cases h_beta
-      have ⟨L1', cbn_L1, std_abs⟩ := Standard.abs_inv std_L _ rfl
-      have std_subst := Standard.abs_subst std_abs std_M (Standard.lc_l std_M) (Standard.lc_r std_M)
-      have step1 : L1.app M1 ↠ₙ L1'.abs.app M1 := CBN.steps_app_l_cong cbn_L1 (Standard.lc_l std_M)
-      have step2 : L1'.abs.app M1 ⭢ₙ L1' ^ M1 :=
-        .base (.beta (CBN.steps_lc_r (Standard.lc_l std_L) cbn_L1) (Standard.lc_l std_M))
-      exact Standard.cbn_trans (.trans step1 (.single step2)) std_subst
+      have ⟨L, cbn_L1, std_abs⟩ := abs_inv std_L _ rfl
+      have std_subst := std_abs.abs_subst std_M std_M.lc_l std_M.lc_r
+      have s1 : L'.app M ↠ₙ L.abs.app M := CBN.steps_app_l_cong cbn_L1 std_M.lc_l
+      have s2 : L.abs.app M ⭢ₙ L ^ M := .base (.beta (CBN.steps_lc_r std_L.lc_l cbn_L1) std_M.lc_l)
+      exact Standard.cbn_trans (.trans s1 (.single s2)) std_subst
 
 /-- A standard reduction followed by a full β-reduction is a standard reduction. -/
 lemma Standard.trans_redex (h1 : M ⭢ₛ P) (h2 : P ↠βᶠ N) : M ⭢ₛ N := by
   induction h2 with
   | refl => exact h1
-  | tail _ step ih => exact Standard.trans_step ih step
+  | tail _ step ih => exact trans_step ih step
 
 /-- Standard reduction is transitive. -/
 lemma Standard.trans (h1 : M ⭢ₛ P) (h2 : P ⭢ₛ N) : M ⭢ₛ N :=
@@ -223,8 +210,8 @@ instance : Trans (· ⭢ₛ · : Term Var → Term Var → Prop) (· ⭢ₛ ·)
 /-- The standardization theorem: every full β-reduction is a standard reduction. -/
 theorem Standard.standardization (lc_M : LC M) (step : M ↠βᶠ N) : M ⭢ₛ N := by
   induction step with
-  | refl => exact Standard.lc_refl M lc_M
-  | tail _ h_step ih => exact ih.trans (Standard.of_beta_step h_step (FullBeta.step_lc_l h_step))
+  | refl => exact lc_refl M lc_M
+  | tail _ h_step ih => exact ih.trans (of_beta_step h_step h_step.step_lc_l)
 
 /-- Standard reduction coincides with full β-reduction on locally closed terms. -/
 theorem Standard.iff_redex (lc_M : LC M) : M ⭢ₛ N ↔ M ↠βᶠ N :=