From c9d16777fd1c762bf2f9a07340dda24e4e4afe9e Mon Sep 17 00:00:00 2001
From: David Wegmann <david.wegmann@fau.de>
Date: Sun, 1 Mar 2026 00:06:35 +0100
Subject: [PATCH 01/12] added helper lemmas for use in the planned strong norm
 proof

---
 .../LocallyNameless/Untyped/FullBeta.lean     | 138 ++++++++++++++++++
 .../LocallyNameless/Untyped/LcAt.lean         |  11 ++
 .../LocallyNameless/Untyped/Properties.lean   |   2 +
 3 files changed, 151 insertions(+)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
index 3ed77b4c5..2b5c79242 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
@@ -8,6 +8,7 @@ module
 
 public import Cslib.Foundations.Data.Relation
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
 
 public section
 
@@ -55,6 +56,8 @@ lemma step_lc_l (step : M ⭢βᶠ M') : LC M := by
   induction step <;> constructor
   all_goals assumption
 
+
+
 /-- Left congruence rule for application in multiple reduction. -/
 @[scoped grind ←]
 theorem redex_app_l_cong (redex : M ↠βᶠ M') (lc_N : LC N) : app M N ↠βᶠ app M' N := by
@@ -74,6 +77,15 @@ lemma step_lc_r (step : M ⭢βᶠ M') : LC M' := by
   case' abs => constructor; assumption
   all_goals grind
 
+lemma steps_lc {M M' : Term Var} (steps : M ↠βᶠ M') (lc_M : LC M) : LC M' := by
+  induction steps <;> grind[FullBeta.step_lc_r]
+
+lemma steps_lc_or_rfl {M M' : Term Var} :
+  M ↠βᶠ M' →
+  LC M' ∨ M = M' := by
+  intro redex
+  cases redex <;> grind[FullBeta.step_lc_r]
+
 /-- Substitution respects a single reduction step. -/
 lemma redex_subst_cong (s s' : Term Var) (x y : Var) (step : s ⭢βᶠ s') :
     s [ x := fvar y ] ⭢βᶠ s' [ x := fvar y ] := by
@@ -86,6 +98,24 @@ lemma redex_subst_cong (s s' : Term Var) (x y : Var) (step : s ⭢βᶠ s') :
   case abs => grind [abs <| free_union Var]
   all_goals grind
 
+/-- Substitution respects a single reduction step. -/
+lemma redex_subst_cong_lc (s s' t : Term Var) (x : Var) (step : s ⭢βᶠ s') (h_lc : LC t) :
+    s [ x := t ] ⭢βᶠ s' [ x := t ] := by
+  induction step
+  case beta m n abs_lc n_lc =>
+    cases abs_lc with | abs xs _ mem =>
+      rw [subst_open x t n m (by grind)]
+      refine beta ?_ (by grind)
+      exact subst_lc (LC.abs xs m mem) h_lc
+  case abs => grind [abs <| free_union Var]
+  all_goals grind
+
+
+
+
+
+
+
 /-- Abstracting then closing preserves a single reduction. -/
 lemma step_abs_close {x : Var} (step : M ⭢βᶠ M') : M⟦0 ↜ x⟧.abs ⭢βᶠ M'⟦0 ↜ x⟧.abs := by
   grind [abs ∅, redex_subst_cong]
@@ -97,6 +127,13 @@ lemma redex_abs_close {x : Var} (step : M ↠βᶠ M') : (M⟦0 ↜ x⟧.abs ↠
   case single ih => exact Relation.ReflTransGen.single (step_abs_close ih)
   case trans l r => exact Relation.ReflTransGen.trans l r
 
+/-- Multiple reduction of opening implies multiple reduction of abstraction. -/
+theorem step_abs_cong (xs : Finset Var) (cofin : ∀ x ∉ xs, (M ^ fvar x) ⭢βᶠ (M' ^ fvar x)) :
+    M.abs ⭢βᶠ M'.abs := by
+  have ⟨fresh, _⟩ := fresh_exists <| free_union [fv] Var
+  rw [open_close fresh M 0 ?_, open_close fresh M' 0 ?_]
+  all_goals grind [step_abs_close]
+
 /-- Multiple reduction of opening implies multiple reduction of abstraction. -/
 theorem redex_abs_cong (xs : Finset Var) (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠βᶠ (M' ^ fvar x)) :
     M.abs ↠βᶠ M'.abs := by
@@ -104,6 +141,107 @@ theorem redex_abs_cong (xs : Finset Var) (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠
   rw [open_close fresh M 0 ?_, open_close fresh M' 0 ?_]
   all_goals grind [redex_abs_close]
 
+theorem redex_abs_fvar_finset_exists (xs : Finset Var)
+  (M M' : Term Var)
+  (step : M.abs ⭢βᶠ M'.abs) :
+  ∃ (L : Finset Var), ∀ x ∉ L, (M ^ fvar x) ⭢βᶠ (M' ^ fvar x) := by
+  cases step
+  case abs L cofin => exists L
+
+
+lemma step_open_cong1 (s s' t : Term Var) (L : Finset Var)
+  (step : ∀ x ∉ L, (s ^ (fvar x)) ⭢βᶠ (s' ^ (fvar x))) (h_lc : LC t) :
+  (s ^ t) ⭢βᶠ (s' ^ t) := by
+  let x := fresh (L ∪ s.fv ∪ s'.fv)
+  have H : x ∉ (L ∪ s.fv ∪ s'.fv) := fresh_notMem (L ∪ s.fv ∪ s'.fv)
+  rw[subst_intro x t s, subst_intro x t s'] <;> simp_all[redex_subst_cong_lc]
+
+lemma invert_steps_abs {s t : Term Var} (step : s.abs ↠βᶠ t) :
+  ∃ (s' : Term Var), s.abs ↠βᶠ s'.abs ∧ t = s'.abs := by
+  induction step
+  · case refl => aesop
+  · case tail steps step ih =>
+      match ih with
+      | ⟨ s', step_s, eq⟩ =>
+        rw[eq] at step
+        cases step
+        · case abs s'' L step =>
+          apply step_abs_cong at step
+          grind
+
+
+
+lemma steps_open_l_abs (s s' t : Term Var)
+  (steps : s.abs ↠βᶠ s'.abs) (lc_s : LC s.abs) (lc_t : LC t) :
+  (s ^ t) ↠βᶠ (s' ^ t) := by
+  generalize eq : s.abs = s_abs at steps
+  generalize eq' : s'.abs = s'_abs at steps
+  revert s s'
+  induction steps
+  · case refl => grind
+  · case tail steps step ih =>
+    intro s s'' lc_sabs eq1 eq2
+    rw[←eq1] at steps
+    match (invert_steps_abs steps) with
+    | ⟨s', step_s, eq⟩ =>
+      specialize (ih s s' lc_sabs eq1 eq.symm)
+      transitivity
+      · apply ih
+      · rw[eq,←eq2] at step
+        apply Relation.ReflTransGen.single
+        have ⟨ L, cofin⟩ := redex_abs_fvar_finset_exists (free_union [fv] Var) s' s'' step
+        apply step_open_cong1
+        · assumption
+        · assumption
+
+lemma step_subst_r {x : Var} (s t t' : Term Var) (step : t ⭢βᶠ t') (h_lc : LC s) :
+    (s [ x := t ]) ↠βᶠ (s [ x := t' ]) := by
+  induction h_lc
+  · case fvar y =>
+      rw[Term.subst_fvar, Term.subst_fvar]
+      grind
+  · case abs L N h_lc ih =>
+      simp[subst_abs]
+      apply FullBeta.redex_abs_cong (L ∪ {x})
+      intro y h_fresh
+      rw[←Term.subst_open_var, ←Term.subst_open_var] <;> try grind[FullBeta.step_lc_r, FullBeta.step_lc_l]
+  · case app l r ih_l ih_r =>
+    transitivity
+    · apply FullBeta.redex_app_r_cong
+      · apply ih_r
+      · grind[Term.subst_lc, FullBeta.step_lc_l]
+    · apply FullBeta.redex_app_l_cong
+      · apply ih_l
+      · grind[Term.subst_lc, FullBeta.step_lc_r]
+
+lemma steps_subst_cong2 {x : Var} (s t t' : Term Var) (step : t ↠βᶠ t') (h_lc : LC s) :
+    (s [ x := t ]) ↠βᶠ (s [ x := t' ]) := by
+  induction step
+  · case refl => rfl
+  · case tail t' t'' steps step ih =>
+    transitivity
+    · apply ih
+    · apply step_subst_r <;> assumption
+
+lemma steps_open_cong_abs (s s' t t' : Term Var)
+    (step1 : t ↠βᶠ t')
+    (step2 : s.abs ↠βᶠ s'.abs)
+    (lc_t : LC t)
+    (lc_s : LC s.abs) :
+    (s ^ t) ↠βᶠ (s' ^ t') := by
+    have lcsabs := lc_s
+    cases lc_s
+    · case abs _ L h_lc =>
+      let x := fresh (L ∪ s.fv ∪ s'.fv ∪ t.fv ∪ t'.fv)
+      have H : x ∉ (L ∪ s.fv ∪ s'.fv ∪ t.fv ∪ t'.fv) := fresh_notMem _
+      rw[subst_intro x t s, subst_intro x t' s'] <;> try grind[FullBeta.steps_lc]
+      · transitivity
+        · apply steps_subst_cong2
+          · assumption
+          · grind
+        · rw[←subst_intro, ←subst_intro] <;> try grind[FullBeta.steps_lc]
+          · apply FullBeta.steps_open_l_abs <;> try grind[FullBeta.steps_lc]
+
 end LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta
 
 end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
index 33b1ba690..c85cf3161 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
@@ -86,4 +86,15 @@ theorem lcAt_iff_LC (M : Term Var) [HasFresh Var] : LcAt 0 M ↔ M.LC := by
         grind [fresh_exists L]
     | _ => grind [cases LC]
 
+theorem lcAt_openRec_lcAt (M N : Term Var) (i : ℕ) :
+    LcAt i (M⟦i ↝ N⟧) → LcAt (i + 1) M := by
+  induction M generalizing i <;> try grind
+
+lemma open_abs_lc [HasFresh Var] : forall {M N : Term Var},
+  LC (M ^ N) → LC (M.abs) := by
+  intro M N hlc
+  rw[←lcAt_iff_LC]
+  rw[←lcAt_iff_LC] at hlc
+  apply lcAt_openRec_lcAt _ _ _ hlc
+
 end Cslib.LambdaCalculus.LocallyNameless.Untyped.Term
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
index f72a8a985..aead7135a 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
@@ -103,6 +103,7 @@ theorem subst_lc {x : Var} {e u : Term Var} (e_lc : LC e) (u_lc : LC u) : LC (e
   case' abs => apply LC.abs (free_union Var)
   all_goals grind
 
+
 /-- Opening to a term `t` is equivalent to opening to a free variable and substituting for `t`. -/
 lemma subst_intro (x : Var) (t e : Term Var) (mem : x ∉ e.fv) (t_lc : LC t) :
     e ^ t = (e ^ fvar x) [ x := t ] := by grind [subst_fresh]
@@ -116,6 +117,7 @@ theorem beta_lc {M N : Term Var} (m_lc : M.abs.LC) (n_lc : LC N) : LC (M ^ N) :=
   cases m_lc with
   | abs => grind [fresh_exists <| free_union [fv] Var]
 
+
 /-- Opening then closing is equivalent to substitution. -/
 @[scoped grind =]
 lemma open_close_to_subst (m : Term Var) (x y : Var) (k : ℕ) (m_lc : LC m) :

From e70160a79cf0172c6319620d783f081fc4632466 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sat, 28 Feb 2026 22:49:44 -0500
Subject: [PATCH 02/12] whitespace in Propertires

---
 .../LambdaCalculus/LocallyNameless/Untyped/Properties.lean      | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
index aead7135a..f72a8a985 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
@@ -103,7 +103,6 @@ theorem subst_lc {x : Var} {e u : Term Var} (e_lc : LC e) (u_lc : LC u) : LC (e
   case' abs => apply LC.abs (free_union Var)
   all_goals grind
 
-
 /-- Opening to a term `t` is equivalent to opening to a free variable and substituting for `t`. -/
 lemma subst_intro (x : Var) (t e : Term Var) (mem : x ∉ e.fv) (t_lc : LC t) :
     e ^ t = (e ^ fvar x) [ x := t ] := by grind [subst_fresh]
@@ -117,7 +116,6 @@ theorem beta_lc {M N : Term Var} (m_lc : M.abs.LC) (n_lc : LC N) : LC (M ^ N) :=
   cases m_lc with
   | abs => grind [fresh_exists <| free_union [fv] Var]
 
-
 /-- Opening then closing is equivalent to substitution. -/
 @[scoped grind =]
 lemma open_close_to_subst (m : Term Var) (x y : Var) (k : ℕ) (m_lc : LC m) :

From 2b7143f787ee4197f8e2fa632117d707dc937a00 Mon Sep 17 00:00:00 2001
From: WegmannDavid <147524946+WegmannDavid@users.noreply.github.com>
Date: Sun, 1 Mar 2026 11:52:46 +0100
Subject: [PATCH 03/12] Apply suggestion from @chenson2018

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
index 2b5c79242..20d2885b2 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
@@ -77,14 +77,8 @@ lemma step_lc_r (step : M ⭢βᶠ M') : LC M' := by
   case' abs => constructor; assumption
   all_goals grind
 
-lemma steps_lc {M M' : Term Var} (steps : M ↠βᶠ M') (lc_M : LC M) : LC M' := by
-  induction steps <;> grind[FullBeta.step_lc_r]
-
-lemma steps_lc_or_rfl {M M' : Term Var} :
-  M ↠βᶠ M' →
-  LC M' ∨ M = M' := by
-  intro redex
-  cases redex <;> grind[FullBeta.step_lc_r]
+lemma steps_lc_or_rfl {M M' : Term Var} (redex : M ↠βᶠ M') : (LC M ∧ LC M') ∨ M = M' := by
+  grind
 
 /-- Substitution respects a single reduction step. -/
 lemma redex_subst_cong (s s' : Term Var) (x y : Var) (step : s ⭢βᶠ s') :

From ec6c1ca02a1277ea883eb88d7cdf0fd3b3cd12a4 Mon Sep 17 00:00:00 2001
From: WegmannDavid <147524946+WegmannDavid@users.noreply.github.com>
Date: Sun, 1 Mar 2026 11:53:09 +0100
Subject: [PATCH 04/12] Apply suggestion from @chenson2018

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
index 20d2885b2..ecfbaeb3f 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
@@ -95,14 +95,10 @@ lemma redex_subst_cong (s s' : Term Var) (x y : Var) (step : s ⭢βᶠ s') :
 /-- Substitution respects a single reduction step. -/
 lemma redex_subst_cong_lc (s s' t : Term Var) (x : Var) (step : s ⭢βᶠ s') (h_lc : LC t) :
     s [ x := t ] ⭢βᶠ s' [ x := t ] := by
-  induction step
-  case beta m n abs_lc n_lc =>
-    cases abs_lc with | abs xs _ mem =>
-      rw [subst_open x t n m (by grind)]
-      refine beta ?_ (by grind)
-      exact subst_lc (LC.abs xs m mem) h_lc
-  case abs => grind [abs <| free_union Var]
-  all_goals grind
+  induction step with
+  | beta => grind [subst_open, beta]
+  | abs  => grind [abs <| free_union Var]
+  | _ => grind
 
 
 

From 5923365928b6db5085cfe2ef179b8bac1d87a99b Mon Sep 17 00:00:00 2001
From: WegmannDavid <147524946+WegmannDavid@users.noreply.github.com>
Date: Sun, 1 Mar 2026 11:53:29 +0100
Subject: [PATCH 05/12] Apply suggestion from @chenson2018

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
index ecfbaeb3f..ea326c99e 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
@@ -139,9 +139,9 @@ theorem redex_abs_fvar_finset_exists (xs : Finset Var)
   case abs L cofin => exists L
 
 
-lemma step_open_cong1 (s s' t : Term Var) (L : Finset Var)
-  (step : ∀ x ∉ L, (s ^ (fvar x)) ⭢βᶠ (s' ^ (fvar x))) (h_lc : LC t) :
-  (s ^ t) ⭢βᶠ (s' ^ t) := by
+lemma step_open_cong
+  (s s' t) (L : Finset Var) (step : ∀ x ∉ L, (s ^ fvar x) ⭢βᶠ (s' ^ fvar x)) (h_lc : LC t) :
+    (s ^ t) ⭢βᶠ (s' ^ t) := by
   let x := fresh (L ∪ s.fv ∪ s'.fv)
   have H : x ∉ (L ∪ s.fv ∪ s'.fv) := fresh_notMem (L ∪ s.fv ∪ s'.fv)
   rw[subst_intro x t s, subst_intro x t s'] <;> simp_all[redex_subst_cong_lc]

From 4763a100722adaf431453c8941d963dd1e774967 Mon Sep 17 00:00:00 2001
From: WegmannDavid <147524946+WegmannDavid@users.noreply.github.com>
Date: Sun, 1 Mar 2026 11:55:50 +0100
Subject: [PATCH 06/12] Apply suggestion from @chenson2018

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
index ea326c99e..051b402fd 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
@@ -142,9 +142,8 @@ theorem redex_abs_fvar_finset_exists (xs : Finset Var)
 lemma step_open_cong
   (s s' t) (L : Finset Var) (step : ∀ x ∉ L, (s ^ fvar x) ⭢βᶠ (s' ^ fvar x)) (h_lc : LC t) :
     (s ^ t) ⭢βᶠ (s' ^ t) := by
-  let x := fresh (L ∪ s.fv ∪ s'.fv)
-  have H : x ∉ (L ∪ s.fv ∪ s'.fv) := fresh_notMem (L ∪ s.fv ∪ s'.fv)
-  rw[subst_intro x t s, subst_intro x t s'] <;> simp_all[redex_subst_cong_lc]
+  have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
+  grind [subst_intro, redex_subst_cong_lc]
 
 lemma invert_steps_abs {s t : Term Var} (step : s.abs ↠βᶠ t) :
   ∃ (s' : Term Var), s.abs ↠βᶠ s'.abs ∧ t = s'.abs := by

From f890c5c6256b63d75f6efd18787b1b941a960da1 Mon Sep 17 00:00:00 2001
From: WegmannDavid <147524946+WegmannDavid@users.noreply.github.com>
Date: Sun, 1 Mar 2026 11:56:01 +0100
Subject: [PATCH 07/12] Apply suggestion from @chenson2018

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
index 051b402fd..bc080c9ab 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
@@ -146,7 +146,7 @@ lemma step_open_cong
   grind [subst_intro, redex_subst_cong_lc]
 
 lemma invert_steps_abs {s t : Term Var} (step : s.abs ↠βᶠ t) :
-  ∃ (s' : Term Var), s.abs ↠βᶠ s'.abs ∧ t = s'.abs := by
+    ∃ (s' : Term Var), s.abs ↠βᶠ s'.abs ∧ t = s'.abs := by
   induction step
   · case refl => aesop
   · case tail steps step ih =>

From 6139222014260ce6a237ce851a0c8242d4b36619 Mon Sep 17 00:00:00 2001
From: WegmannDavid <147524946+WegmannDavid@users.noreply.github.com>
Date: Sun, 1 Mar 2026 11:56:27 +0100
Subject: [PATCH 08/12] Apply suggestion from @chenson2018

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
index bc080c9ab..3084a6d0d 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
@@ -147,16 +147,9 @@ lemma step_open_cong
 
 lemma invert_steps_abs {s t : Term Var} (step : s.abs ↠βᶠ t) :
     ∃ (s' : Term Var), s.abs ↠βᶠ s'.abs ∧ t = s'.abs := by
-  induction step
-  · case refl => aesop
-  · case tail steps step ih =>
-      match ih with
-      | ⟨ s', step_s, eq⟩ =>
-        rw[eq] at step
-        cases step
-        · case abs s'' L step =>
-          apply step_abs_cong at step
-          grind
+  induction step with
+  | refl => grind
+  | tail _ step _ => cases step with grind [step_abs_cong (free_union Var)]
 
 
 

From c9e3055536a8adb57a1a70b0a772b803f1acf051 Mon Sep 17 00:00:00 2001
From: WegmannDavid <147524946+WegmannDavid@users.noreply.github.com>
Date: Sun, 1 Mar 2026 11:56:56 +0100
Subject: [PATCH 09/12] Apply suggestion from @chenson2018

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
index 3084a6d0d..aab35eb87 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
@@ -153,28 +153,16 @@ lemma invert_steps_abs {s t : Term Var} (step : s.abs ↠βᶠ t) :
 
 
 
-lemma steps_open_l_abs (s s' t : Term Var)
-  (steps : s.abs ↠βᶠ s'.abs) (lc_s : LC s.abs) (lc_t : LC t) :
-  (s ^ t) ↠βᶠ (s' ^ t) := by
+lemma steps_open_l_abs
+  (s s' t : Term Var) (steps : s.abs ↠βᶠ s'.abs) (lc_s : LC s.abs) (lc_t : LC t) :
+    (s ^ t) ↠βᶠ (s' ^ t) := by
   generalize eq : s.abs = s_abs at steps
   generalize eq' : s'.abs = s'_abs at steps
-  revert s s'
-  induction steps
-  · case refl => grind
-  · case tail steps step ih =>
-    intro s s'' lc_sabs eq1 eq2
-    rw[←eq1] at steps
-    match (invert_steps_abs steps) with
-    | ⟨s', step_s, eq⟩ =>
-      specialize (ih s s' lc_sabs eq1 eq.symm)
-      transitivity
-      · apply ih
-      · rw[eq,←eq2] at step
-        apply Relation.ReflTransGen.single
-        have ⟨ L, cofin⟩ := redex_abs_fvar_finset_exists (free_union [fv] Var) s' s'' step
-        apply step_open_cong1
-        · assumption
-        · assumption
+  induction steps generalizing s s' with
+  | refl => grind
+  | tail _ step ih =>
+    specialize ih s
+    cases step with grind [invert_steps_abs, step_open_cong (L := free_union Var)]
 
 lemma step_subst_r {x : Var} (s t t' : Term Var) (step : t ⭢βᶠ t') (h_lc : LC s) :
     (s [ x := t ]) ↠βᶠ (s [ x := t' ]) := by

From 13a860bb3b211d579f82b010b62b198a2c17d5ef Mon Sep 17 00:00:00 2001
From: WegmannDavid <147524946+WegmannDavid@users.noreply.github.com>
Date: Sun, 1 Mar 2026 11:58:38 +0100
Subject: [PATCH 10/12] Apply suggestion from @chenson2018

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
index aab35eb87..d759f3aa0 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
@@ -166,23 +166,13 @@ lemma steps_open_l_abs
 
 lemma step_subst_r {x : Var} (s t t' : Term Var) (step : t ⭢βᶠ t') (h_lc : LC s) :
     (s [ x := t ]) ↠βᶠ (s [ x := t' ]) := by
-  induction h_lc
-  · case fvar y =>
-      rw[Term.subst_fvar, Term.subst_fvar]
-      grind
-  · case abs L N h_lc ih =>
-      simp[subst_abs]
-      apply FullBeta.redex_abs_cong (L ∪ {x})
-      intro y h_fresh
-      rw[←Term.subst_open_var, ←Term.subst_open_var] <;> try grind[FullBeta.step_lc_r, FullBeta.step_lc_l]
-  · case app l r ih_l ih_r =>
-    transitivity
-    · apply FullBeta.redex_app_r_cong
-      · apply ih_r
-      · grind[Term.subst_lc, FullBeta.step_lc_l]
-    · apply FullBeta.redex_app_l_cong
-      · apply ih_l
-      · grind[Term.subst_lc, FullBeta.step_lc_r]
+  induction h_lc with
+  | fvar y => grind
+  | abs => grind [redex_abs_cong (free_union Var)]
+  | @app l r =>
+     calc
+       (l.app r)[x:=t] ↠βᶠ l[x := t].app (r[x:=t']) := by grind
+       _               ↠βᶠ (l.app r)[x:=t'] := by grind
 
 lemma steps_subst_cong2 {x : Var} (s t t' : Term Var) (step : t ↠βᶠ t') (h_lc : LC s) :
     (s [ x := t ]) ↠βᶠ (s [ x := t' ]) := by

From 40b226d928790e4c925694cbff1b3a159254703e Mon Sep 17 00:00:00 2001
From: WegmannDavid <147524946+WegmannDavid@users.noreply.github.com>
Date: Sun, 1 Mar 2026 11:58:51 +0100
Subject: [PATCH 11/12] Apply suggestion from @chenson2018

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
index c85cf3161..fb9770f8a 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
@@ -88,7 +88,7 @@ theorem lcAt_iff_LC (M : Term Var) [HasFresh Var] : LcAt 0 M ↔ M.LC := by
 
 theorem lcAt_openRec_lcAt (M N : Term Var) (i : ℕ) :
     LcAt i (M⟦i ↝ N⟧) → LcAt (i + 1) M := by
-  induction M generalizing i <;> try grind
+  induction M generalizing i <;> grind
 
 lemma open_abs_lc [HasFresh Var] : forall {M N : Term Var},
   LC (M ^ N) → LC (M.abs) := by

From 50ed9671ff9568fab8f237fdb8b6aa8ac128a8ec Mon Sep 17 00:00:00 2001
From: WegmannDavid <147524946+WegmannDavid@users.noreply.github.com>
Date: Sun, 1 Mar 2026 12:00:48 +0100
Subject: [PATCH 12/12] Apply suggestion from @chenson2018

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
index d759f3aa0..936ad3ebe 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
@@ -189,18 +189,14 @@ lemma steps_open_cong_abs (s s' t t' : Term Var)
     (lc_t : LC t)
     (lc_s : LC s.abs) :
     (s ^ t) ↠βᶠ (s' ^ t') := by
-    have lcsabs := lc_s
-    cases lc_s
-    · case abs _ L h_lc =>
-      let x := fresh (L ∪ s.fv ∪ s'.fv ∪ t.fv ∪ t'.fv)
-      have H : x ∉ (L ∪ s.fv ∪ s'.fv ∪ t.fv ∪ t'.fv) := fresh_notMem _
-      rw[subst_intro x t s, subst_intro x t' s'] <;> try grind[FullBeta.steps_lc]
-      · transitivity
-        · apply steps_subst_cong2
-          · assumption
-          · grind
-        · rw[←subst_intro, ←subst_intro] <;> try grind[FullBeta.steps_lc]
-          · apply FullBeta.steps_open_l_abs <;> try grind[FullBeta.steps_lc]
+    cases lc_s with
+    | abs L h_lc =>
+      have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
+      rw [subst_intro x t s, subst_intro x t' s']
+      · trans (s ^ fvar x)[x:=t']
+        · grind [steps_subst_cong2]
+        · grind [=_ subst_intro, steps_open_l_abs]
+      all_goals grind
 
 end LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta