From 3c41d959274dfcb9955c1ed10b540a33feb2be3a Mon Sep 17 00:00:00 2001
From: David Wegmann <david.wegmann@fau.de>
Date: Fri, 6 Mar 2026 04:47:54 +0100
Subject: [PATCH 01/22] changes to MultiSubst.lean

---
 .../LocallyNameless/Stlc/StrongNorm.lean      | 175 ++++++++++++++
 .../LocallyNameless/Untyped/FullBeta.lean     | 191 +++++++++++-----
 .../LocallyNameless/Untyped/LcAt.lean         |  18 +-
 .../LocallyNameless/Untyped/MultiApp.lean     | 149 ++++++++++++
 .../LocallyNameless/Untyped/MultiSubst.lean   | 130 +++++++++++
 .../LocallyNameless/Untyped/Properties.lean   |   2 +
 .../LocallyNameless/Untyped/StrongNorm.lean   | 216 ++++++++++++++++++
 7 files changed, 809 insertions(+), 72 deletions(-)
 create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
 create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
 create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean
 create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
new file mode 100644
index 000000000..ba3db50f6
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
@@ -0,0 +1,175 @@
+module
+
+import Cslib.Foundations.Data.Relation
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
+
+namespace Cslib
+
+universe u v
+
+namespace LambdaCalculus.LocallyNameless.Stlc
+
+open Untyped Typing LambdaCalculus.LocallyNameless.Untyped.Term
+
+variable {Var : Type u} {Base : Type v} [DecidableEq Var] [HasFresh Var]
+
+open LambdaCalculus.LocallyNameless.Stlc
+open scoped Term
+
+
+
+inductive saturated (S : Set (Term Var)) : Prop :=
+| intro : (∀ M ∈ S, LC M) →
+          (∀ M ∈ S, SN M) →
+          (∀ M, neutral M → LC M → M ∈ S) →
+          (∀ M N P, LC N → SN N → multiApp (M ^ N) P ∈ S → multiApp ((Term.abs M).app N) P ∈ S) →
+          saturated S
+
+
+@[simp]
+def semanticMap (τ : Ty Base) : Set (Term Var) :=
+  match τ with
+  | Ty.base _ => { t : Term Var | SN t ∧ LC t }
+  | Ty.arrow τ₁ τ₂ =>
+    { t : Term Var | ∀ s : Term Var, s ∈ semanticMap τ₁ → (Term.app t s) ∈ semanticMap τ₂ }
+
+
+
+def semanticMap_saturated (τ : Ty Base) :
+    @saturated Var (semanticMap τ) := by
+  induction τ
+  · case base b =>
+      constructor
+      · simp_all
+      · simp_all
+      · simp_all[neutral_sn]
+      · intro M N P lc_N sn_N h_app
+        constructor
+        · simp_all[multiApp_sn]
+        · have H := h_app.2
+          rw[multiApp_lc] at *
+          grind[open_abs_lc]
+  · case arrow τ₁ τ₂ ih₁ ih₂ =>
+      constructor
+      · intro M hM
+        have H := ih₁.3 (.fvar (fresh {})) (.fvar (fresh {})) (.fvar (fresh {}))
+        specialize (hM (fvar (fresh {})) H)
+        apply (ih₂.1) at hM
+        cases hM
+        assumption
+      · intro M hM
+        apply sn_app_left M (Term.fvar (fresh {}))
+        · constructor
+        · have H := ih₁.3 (.fvar (fresh {})) (.fvar (fresh {})) (.fvar (fresh {}))
+          specialize (hM (fvar (fresh {})) H)
+          apply ih₂.2 ; assumption
+      · intro M hneut mlc s hs
+        apply ih₂.3
+        · constructor
+          · assumption
+          · apply ih₁.2
+            assumption
+        · constructor
+          · assumption
+          · apply ih₁.1
+            assumption
+      · intro M N P lc_N sn_N h_app s hs
+        apply ih₂.4 M N (s::P)
+        · apply lc_N
+        · apply sn_N
+        · apply h_app
+          assumption
+
+
+
+
+
+def entails_context (Ns : Term.Environment Var) (Γ : Context Var (Ty Base)) :=
+  ∀ {x τ}, ⟨ x, τ ⟩ ∈ Γ → (multiSubst Ns (Term.fvar x)) ∈ semanticMap τ
+
+lemma entails_context_empty {Γ : Context Var (Ty Base)} :
+  entails_context [] Γ := by
+  intro x τ h_mem
+  rw[multiSubst]
+  apply (semanticMap_saturated τ).3 <;> constructor
+
+
+lemma entails_context_cons (Ns : Term.Environment Var) (Γ : Context Var (Ty Base))
+  (x : Var) (τ : Ty Base) (sub : Term Var) :
+  x ∉ Ns.dom ∪ Ns.fv ∪ Γ.dom →
+  sub ∈ semanticMap τ →
+  entails_context Ns Γ → entails_context (⟨ x, sub ⟩ :: Ns) (⟨ x, τ ⟩ :: Γ) := by
+  intro h_fresh h_mem h_entails y σ h_mem
+  rw[multiSubst]
+  rw[entails_context] at h_entails
+  cases h_mem
+  · case head =>
+    rw[multiSubst_fvar_fresh]
+    · rw[subst_fvar]
+      simp_all
+    · simp_all
+  · case tail h_mem =>
+    specialize (h_entails h_mem)
+    rw [subst_fresh]
+    · assumption
+    · apply multiSubst_preserves_not_fvar
+      apply List.mem_keys_of_mem at h_mem
+      aesop
+
+
+def entails (Γ : Context Var (Ty Base)) (t : Term Var) (τ : Ty Base) :=
+  ∀ Ns, env_LC Ns → (entails_context Ns Γ) → (multiSubst Ns t) ∈ semanticMap τ
+
+
+theorem soundness {Γ : Context Var (Ty Base)} {t : Term Var} {τ : Ty Base} :
+  Γ ⊢ t ∶ τ → entails Γ t τ := by
+  intro derivation_t
+  induction derivation_t
+  · case var Γ xσ_mem_Γ =>
+      intro Ns lc_Ns hsat
+      apply hsat xσ_mem_Γ
+  · case' abs σ Γ t τ L IH derivation_t =>
+      intro Ns lc_Ns hsat s hsat_s
+      rw[multiSubst_abs]
+      apply (semanticMap_saturated _).4 _ _ []
+      · apply (semanticMap_saturated _).1
+        assumption
+      · apply (semanticMap_saturated _).2
+        assumption
+      · rw[multiApp]
+        set x := fresh (t.fv ∪ L ∪ Ns.dom ∪ Ns.fv ∪ Context.dom Γ ∪ (multiSubst Ns t).fv)
+        have hfresh : x ∉ t.fv ∪ L ∪ Ns.dom ∪ Ns.fv ∪ Context.dom Γ  ∪ (multiSubst Ns t).fv := by apply fresh_notMem
+        have hfreshL : x ∉ L := by simp_all
+        have H1 := derivation_t x hfreshL
+        rw[entails] at H1
+        specialize H1 (⟨x,s⟩ :: Ns)
+        rw [multiSubst, multiSubst_open_var, ←subst_intro] at H1
+        · apply H1
+          · apply env_LC_cons
+            · apply (semanticMap_saturated _).1
+              assumption
+            · assumption
+          · apply entails_context_cons <;> simp_all
+        · simp_all
+        · apply (semanticMap_saturated σ).1
+          assumption
+        · simp_all
+        · aesop
+  · case app derivation_t derivation_t' IH IH' =>
+      intro Ns lc_Ns hsat
+      rw[multiSubst_app]
+      apply IH Ns lc_Ns hsat
+      apply IH' Ns lc_Ns hsat
+
+theorem strong_norm {Γ} {t : Term Var} {τ : Ty Base} (der : Γ ⊢ t ∶ τ) : SN t := by
+  have H := soundness der [] (by aesop) entails_context_empty
+  apply (semanticMap_saturated τ).2
+  assumption
+
+end LambdaCalculus.LocallyNameless.Stlc
+
+end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
index 742f000b4..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,21 +77,44 @@ lemma step_lc_r (step : M ⭢βᶠ M') : LC M' := by
   case' abs => constructor; assumption
   all_goals grind
 
-lemma steps_lc_or_rfl {M M' : Term Var} (redex : M ↠βᶠ M') : (LC M ∧ LC M') ∨ M = M' := by
-  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 of a locally closed term respects a single reduction step. -/
+/-- 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
+  induction step
+  case beta m n abs_lc n_lc =>
+    cases abs_lc with | abs xs _ mem =>
+      rw [subst_open x (fvar y) n m (by grind)]
+      refine beta ?_ (by grind)
+      exact subst_lc (LC.abs xs m mem) (LC.fvar y)
+  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 with
-  | beta => grind [subst_open, beta]
-  | abs  => grind [abs <| free_union Var]
-  | _ => grind
+  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
+
+
+
+
+
 
-/-- Substitution respects a single reduction step of a free variable. -/
-lemma redex_subst_cong (s s' : Term Var) (x y : Var) (step : s ⭢βᶠ s') :
-    s [ x := fvar y ] ⭢βᶠ s' [ x := fvar y ] :=
-  redex_subst_cong_lc _ _ _ _ step (.fvar y)
 
 /-- 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
@@ -115,67 +141,106 @@ 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]
 
-/- Reduction is preserved when opening with a locally closed term. -/
-lemma step_open_cong_l
-  (s s' t) (L : Finset Var) (step : ∀ x ∉ L, (s ^ fvar x) ⭢βᶠ (s' ^ fvar x)) (h_lc : LC t) :
-    (s ^ t) ⭢βᶠ (s' ^ t) := by
-  have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
-  grind [subst_intro, redex_subst_cong_lc]
+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]
 
-/- Multiple reduction `λ s ↠βᶠ t` implies `t = λ s'` for some s' -/
 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 with
-  | refl => grind
-  | tail _ step _ => cases step with grind [step_abs_cong (free_union Var)]
-
-/- `λ s ↠βᶠ λ s'` implies `s ^ t ↠βᶠ s' ^ t'` -/
-lemma steps_open_cong_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
+  ∃ (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
-  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 (L := free_union Var)]
-
-/- `t ↠βᶠ t'` implies `s [ x := t ] ↠βᶠ s [ x := t' ]`.
-   There is no single step lemma in this case because x
-   may be substituted for n times, so a single step t ↠βᶠ t
-   in general requires n steps in `s [ x := t ] ↠βᶠ (s [ x := t' ])` -/
-lemma step_subst_cong_r {x : Var} (s t t' : Term Var) (step : t ⭢βᶠ t') (h_lc : LC s) :
+  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 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
-
-/- `step_subst_cong_r` can be generalized to multiple reductions `t ↠βᶠ t'`.
-   This requires s to be locally closed, locally closedness of t and t'
-   can be infered by the fact t reduces to t' -/
-lemma steps_subst_cong_r {x : Var} (s t t' : Term Var) (step : t ↠βᶠ t') (h_lc : LC s) :
+  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 with
-  | refl => rfl
-  | tail steps step ih => grind [Relation.ReflTransGen.trans, step_subst_cong_r]
+  induction step
+  · case refl => rfl
+  · case tail t' t'' steps step ih =>
+    transitivity
+    · apply ih
+    · apply step_subst_r <;> assumption
 
-/- When both `t` and `s` reduce to `t'` and `s'`, then `t ^ s` reduces to `t' ^ s'` -/
 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) :
+    (step1 : t ↠βᶠ t')
+    (step2 : s.abs ↠βᶠ s'.abs)
+    (lc_t : LC t)
+    (lc_s : LC s.abs) :
     (s ^ t) ↠βᶠ (s' ^ t') := by
-  cases lc_s with
-  | abs L =>
-    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_cong_r]
-      · grind [=_ subst_intro, steps_open_cong_l_abs]
-    all_goals grind
+    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
 
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
index 092c176c1..c85cf3161 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
@@ -86,15 +86,15 @@ theorem lcAt_iff_LC (M : Term Var) [HasFresh Var] : LcAt 0 M ↔ M.LC := by
         grind [fresh_exists L]
     | _ => grind [cases LC]
 
-/- Opening for some term at i-th bound variable increments `LcAt` by one -/
-lemma lcAt_openRec_lcAt (M N : Term Var) (i : ℕ) :
+theorem lcAt_openRec_lcAt (M N : Term Var) (i : ℕ) :
     LcAt i (M⟦i ↝ N⟧) → LcAt (i + 1) M := by
-  induction M generalizing i <;> grind
-
-/- When `M ^ N` is locally closed, then `M.abs` is locally closed. This is proven by translating LC
-   to LcAt, applying lcAt_openRec_lcAt, then translating back to LC -/
-lemma open_abs_lc [HasFresh Var] {M N : Term Var} (hlc : LC (M ^ N)) : LC (M.abs) := by
-  rw [← lcAt_iff_LC] at *
-  exact lcAt_openRec_lcAt _ _ _ hlc
+  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/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
new file mode 100644
index 000000000..312b8a6c8
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -0,0 +1,149 @@
+module
+
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
+
+@[expose] public section
+
+namespace Cslib
+
+universe u
+
+variable {Var : Type u} [DecidableEq Var] [HasFresh Var]
+
+namespace LambdaCalculus.LocallyNameless.Untyped.Term
+
+@[simp]
+def multiApp (f : Term Var) (args : List (Term Var)) :=
+  match args with
+  | []      => f
+  | a :: as => Term.app (multiApp f as) a
+
+@[reduction_sys "βᶠ"]
+inductive multiApp_full_beta : List (Term Var) → List (Term Var) → Prop where
+| step : N ⭢βᶠ N' → (∀ N ∈ Ns, LC N) → multiApp_full_beta (N :: Ns) (N' :: Ns)
+| cons : LC N → multiApp_full_beta Ns Ns' → multiApp_full_beta (N :: Ns) (N :: Ns')
+
+attribute [scoped grind .] multiApp_full_beta.step multiApp_full_beta.cons
+
+lemma multiApp_step_lc_r {Ns Ns' : List (Term Var)}
+  (step : Ns ⭢βᶠ Ns')
+  : (∀ N ∈ Ns', LC N) := by
+  induction step <;> grind[FullBeta.step_lc_r]
+
+lemma multiApp_steps_lc {Ns Ns' : List (Term Var)}
+  (step : Ns ↠βᶠ Ns') (H : ∀ N ∈ Ns, LC N)
+  : (∀ N ∈ Ns', LC N) := by
+  induction step <;> grind[FullBeta.step_lc_r, multiApp_step_lc_r]
+
+@[scoped grind ←]
+lemma multiApp_lc {M : Term Var} {Ns : List (Term Var)} :
+  LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N)
+   := by
+  constructor
+  · induction Ns
+    · case nil => grind[multiApp]
+    · case cons N Ns ih => intro h_lc; cases h_lc; grind
+  · induction Ns <;> grind[multiApp, LC.app]
+
+@[scoped grind ←]
+lemma step_multiApp_l {M M' : Term Var} {Ns : List (Term Var)} :
+  M ⭢βᶠ M' →
+  (∀ N ∈ Ns, LC N) →
+  M.multiApp Ns ⭢βᶠ M'.multiApp Ns := by
+  induction Ns <;> grind[multiApp, FullBeta.appR]
+
+@[scoped grind ←]
+lemma steps_multiApp_l {M M' : Term Var} {Ns : List (Term Var)}
+  (steps : M ↠βᶠ M')
+  (lc_Ns : ∀ N ∈ Ns, LC N)
+  : M.multiApp Ns ↠βᶠ M'.multiApp Ns := by
+  induction steps <;> grind
+
+@[scoped grind ←]
+lemma step_multiApp_r {M : Term Var} {Ns Ns' : List (Term Var)}
+  (steps : Ns ⭢βᶠ Ns')
+  (lc_M : LC M)
+  : M.multiApp Ns ⭢βᶠ M.multiApp Ns' := by
+  induction steps <;> grind[multiApp,FullBeta.appL,FullBeta.appR]
+
+@[scoped grind ←]
+lemma steps_multiApp_r {M : Term Var} {Ns Ns' : List (Term Var)}
+  (steps : Ns ↠βᶠ Ns')
+  (lc_M : LC M)
+  : M.multiApp Ns ↠βᶠ M.multiApp Ns' := by
+  induction steps <;> grind[multiApp,FullBeta.appL,FullBeta.appR]
+
+lemma invert_multiApp_st {Ps} {M N Q : Term Var}
+  (h_red : multiApp (M.abs.app N) Ps ⭢βᶠ Q) :
+  (∃ M', M.abs ⭢βᶠ Term.abs M' ∧ Q = multiApp (M'.abs.app N) Ps) ∨
+  (∃ N', N ⭢βᶠ N' ∧ Q = multiApp (M.abs.app N') Ps) ∨
+  (∃ Ps', Ps ⭢βᶠ Ps' ∧ Q = multiApp (M.abs.app N) Ps') ∨
+  (Q = multiApp (M ^ N) Ps) := by
+  revert M N Q h_red
+  induction Ps with
+  | nil =>
+    intro N N P h_red
+    rw[multiApp] at h_red
+    rw[multiApp]
+    cases h_red
+    · case beta abs_lc n_lc => aesop
+    · case appL M N' lc_z h_red => aesop
+    · case appR M M' lc_z h_red =>
+        left
+        cases lc_z
+        · case abs M' xs h_lc =>
+            exists M'
+            constructor
+            · apply FullBeta.step_abs_cong
+              assumption
+            · rfl
+  | cons P Ps ih =>
+    intro M N Q h_red
+    have h_lc := (FullBeta.step_lc_l h_red)
+    rw [multiApp] at h_red
+    generalize Heq : (M.abs.app N).multiApp Ps = Q'
+    rw[Heq] at h_red
+    cases h_red
+    · case beta abs_lc n_lc => cases Ps <;> contradiction
+    · case appL Y M P' lc_z h_red =>
+        right; right; left
+        exists (P' :: Ps)
+        simp
+        grind
+    · case appR M Q'' h_red P_lc =>
+        rw[←Heq] at h_red
+        match (ih h_red) with
+        | .inl ⟨ M', st, Heq' ⟩                => aesop
+        | .inr (.inl ⟨ N', st, Heq' ⟩)         => aesop
+        | .inr (.inr (.inl ⟨ Ps', st, Heq' ⟩)) =>
+          right; right; left
+          exists (P :: Ps')
+          simp
+          grind
+        | .inr (.inr (.inr Heq'))              => aesop
+
+
+lemma invert_multiApp_mst {Ps} {M N Q : Term Var}
+  (h_red : multiApp (M.abs.app N) Ps ↠βᶠ Q) :
+  ∃ M' N' Ns', M.abs ↠βᶠ M'.abs ∧ N ↠βᶠ N' ∧ Ps ↠βᶠ Ns' ∧
+    (Q = multiApp (M'.abs.app N') Ns' ∨
+     (multiApp (M.abs.app N) Ps ↠βᶠ multiApp (M'^ N') Ns' ∧
+                                      multiApp (M'^ N') Ns' ↠βᶠ Q)) := by
+  induction h_red
+  · case refl => grind
+  · case tail Q' Q'' steps step ih =>
+    match ih with
+    | ⟨ M', N', Ps', st_M, st_N, st_Ps, Cases ⟩ =>
+      match Cases with
+      | .inl Heq =>
+        rw[Heq] at step
+        match (invert_multiApp_st step) with
+        | .inl ⟨ M'', st, HeqM'' ⟩             => grind
+        | .inr (.inl ⟨ N', st, Heq' ⟩)         => grind
+        | .inr (.inr (.inl ⟨ Ps', st, Heq' ⟩)) => grind
+        | .inr (.inr (.inr Heq'))              => grind
+      | .inr ⟨ steps1, steps2 ⟩ => grind[Relation.ReflTransGen.single]
+
+end LambdaCalculus.LocallyNameless.Untyped.Term
+
+end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean
new file mode 100644
index 000000000..6693f6d53
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean
@@ -0,0 +1,130 @@
+module
+
+public import Cslib.Foundations.Data.Relation
+public import Cslib.Foundations.Data.HasFresh
+public import Cslib.Foundations.Syntax.HasSubstitution
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
+
+
+@[expose] public section
+
+namespace Cslib
+
+universe u v
+
+
+namespace LambdaCalculus.LocallyNameless.Untyped.Term
+
+variable {Var : Type u} {Base : Type v} [DecidableEq Var] [HasFresh Var]
+
+
+abbrev Environment (Var : Type u) := Context Var (Term Var)
+
+def multiSubst (σ : Environment Var) (M : Term Var) : Term Var :=
+  match σ with
+  | [] => M
+  | ⟨ i, sub ⟩ :: σ' => (multiSubst σ' M) [ i := sub ]
+
+def Environment.fv (Ns : Environment Var) : Finset Var :=
+  match Ns with
+  | [] => {}
+  | ⟨ _, sub ⟩ :: Ns' => sub.fv ∪ fv Ns'
+
+
+@[simp]
+def env_LC (Γ : Environment Var) : Prop :=
+  ∀ {x M}, ⟨ x, M ⟩ ∈ Γ → LC M
+
+lemma env_LC_cons {Γ : Environment Var} {x : Var} {sub : Term Var}
+  (lc_sub : LC sub)
+  (lc_Γ : env_LC Γ)
+  : env_LC (⟨ x, sub ⟩ :: Γ) := by
+  intro y M h_mem
+  cases h_mem <;> aesop
+
+
+
+def multiSubst_fvar_fresh (Ns : Environment Var) :
+  ∀ x ∉ Ns.dom, multiSubst Ns (Term.fvar x) = Term.fvar x := by
+  induction Ns <;> intro x h_fresh
+  · case nil =>
+      simp [multiSubst]
+  · case cons N Ns ih =>
+      simp only [multiSubst]
+      simp only [Context.dom] at h_fresh
+      rw[ih]
+      · rw[subst_fvar]
+        by_cases h : N.1 = x <;> simp_all
+      · simp_all
+
+lemma multiSubst_preserves_not_fvar {x : Var}
+  (M : Term Var)
+  (Ns : Environment Var)
+  (nmem : x ∉ M.fv ∪ Ns.fv) :
+  x ∉ (multiSubst Ns M).fv := by
+  induction Ns
+  · case nil =>
+      rw[multiSubst]
+      simp_all
+  · case cons N Ns ih =>
+      rw[multiSubst]
+      apply subst_preserve_not_fvar
+      rw[Environment.fv] at nmem
+      simp_all
+
+def multiSubst_app (M N : Term Var) (Ps : Environment Var) :
+        multiSubst Ps (Term.app M N) = Term.app (multiSubst Ps M) (multiSubst Ps N) := by
+  induction Ps
+  · rfl
+  · case cons N Ns ih => rw[multiSubst, multiSubst, ih]; rfl
+
+def multiSubst_abs (M : Term Var) (Ns : Environment Var) :
+    multiSubst Ns (Term.abs M) =
+    Term.abs (multiSubst Ns M) := by
+  induction Ns
+  · rfl
+  · case cons N Ns ih => rw[multiSubst, ih]; rfl
+
+lemma open'_fvar_subst (M N : Term Var) (x : Var) (H : x ∉ Term.fv M) :
+  (i : Nat) → (M ⟦ i ↝ Term.fvar x ⟧) [x := N] = M ⟦ i ↝ N ⟧ := by
+  induction M <;> intro i
+  · case bvar j =>
+      rw[Term.openRec_bvar, Term.openRec_bvar]
+      by_cases h : i = j <;> simp[h, Term.subst_fvar, Term.subst_bvar]
+  · case fvar y =>
+      rw[Term.openRec_fvar, Term.openRec_fvar]
+      simp only [Term.fv, Finset.mem_singleton] at H
+      simp only [subst_fvar, ite_eq_right_iff]
+      intro H
+      contradiction
+  · case abs M ih =>
+      rw[Term.openRec_abs, Term.openRec_abs]
+      rw[Term.subst_abs]
+      rw[ih H]
+  · case app l r ih_l ih_r =>
+      rw[Term.openRec_app, Term.openRec_app]
+      rw[Term.subst_app]
+      simp only [Term.fv, Finset.mem_union, not_or] at H
+      rw[ih_l H.1]
+      rw[ih_r H.2]
+
+lemma multiSubst_open_var (M : Term Var) (Ns : Environment Var) (x : Var) :
+  x ∉ Ns.dom →
+  env_LC Ns →
+  (multiSubst Ns (M ^ (Term.fvar x))) =
+  (multiSubst Ns M) ^ (Term.fvar x) := by
+  intro h_ndom h_lc
+  induction Ns with
+  | nil => rfl
+  | cons N Ns ih =>
+    rw[multiSubst, multiSubst]
+    rw[ih]
+    · rw[subst_open_var] <;> aesop
+    · simp_all
+    aesop
+
+end LambdaCalculus.LocallyNameless.Untyped.Term
+
+end Cslib
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) :
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
new file mode 100644
index 000000000..01f673c1d
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
@@ -0,0 +1,216 @@
+module
+
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
+
+@[expose] public section
+
+namespace Cslib
+
+universe u
+
+variable {Var : Type u} [DecidableEq Var] [HasFresh Var]
+
+
+namespace LambdaCalculus.LocallyNameless.Untyped.Term
+
+attribute [grind =] Finset.union_singleton
+
+
+inductive SN {α} : Term α → Prop
+| sn t : (∀ (t' : Term α), (t ⭢βᶠ t') → SN t') → SN t
+
+@[aesop safe]
+lemma sn_step {t t' : Term Var} (t_st_t' : t ⭢βᶠ t') (sn_t : SN t) : SN t' := by
+  cases sn_t; grind
+
+@[aesop safe]
+lemma sn_mst {t t' : Term Var} (t_st_t' : t ↠βᶠ t') (sn_t : SN t) : SN t' := by
+  induction t_st_t' <;> grind[sn_step]
+
+lemma sn_fvar {x : Var} : SN (Term.fvar x) := by
+  constructor
+  intro t' hstep
+  cases hstep
+
+lemma sn_app (t s : Term Var) :
+  SN t →
+  SN s →
+  (∀ {t' s' : Term Var}, t ↠βᶠ t'.abs → s ↠βᶠ s' → SN (t' ^ s')) →
+  SN (t.app s) := by
+  intro h_sn_t h_sn_s hβ
+  induction h_sn_t generalizing s with | sn t ht ih_t =>
+  induction h_sn_s with | sn s hs ih_s =>
+  constructor
+  intro u hstep
+  cases hstep with
+  | beta _ _ => apply hβ <;> rfl
+  | appL _ h_s_red =>
+    apply ih_s _ h_s_red
+    intro t' s'' hstep1 hstep2
+    exact hβ hstep1 (Relation.ReflTransGen.head h_s_red hstep2)
+  | appR _ h_t_red =>
+    apply ih_t _ h_t_red _ (SN.sn s hs)
+    intro t' s' hstep1 hstep2
+    exact hβ (Relation.ReflTransGen.head h_t_red hstep1) hstep2
+
+
+
+lemma sn_app_left (M N : Term Var) : Term.LC N → SN (M.app N) → SN M := by
+  intro lc_N h_sn
+  generalize Heq : M.app N = P
+  rw[Heq] at h_sn
+  revert M N
+  induction h_sn
+  · case sn P h_sn ih =>
+    intro M N lc_N Heq
+    rw[←Heq] at ih
+    constructor
+    intro M' h_step
+    apply ih (M'.app N)
+    apply Term.FullBeta.appR <;> assumption
+    · assumption
+    · rfl
+
+lemma sn_app_right (M N : Term Var) : Term.LC M → SN (M.app N) → SN N := by
+  intro lc_N h_sn
+  generalize Heq : M.app N = P
+  rw[Heq] at h_sn
+  revert M N
+  induction h_sn
+  · case sn P h_sn ih =>
+    intro M N lc_N Heq
+    rw[←Heq] at ih
+    constructor
+    intro N' h_step
+    apply ih (M.app N')
+    apply Term.FullBeta.appL <;> assumption
+    · assumption
+    · rfl
+
+@[aesop safe constructors]
+inductive neutral : Term Var → Prop
+| bvar : ∀ n, neutral (Term.bvar n)
+| fvar : ∀ x, neutral (Term.fvar x)
+| app : ∀ t1 t2, neutral t1 → SN t2 → neutral (Term.app t1 t2)
+
+@[aesop safe]
+lemma neutral_step {t : Term Var} :
+  neutral t → ∀ t', t ⭢βᶠ t' → neutral t' := by
+  intro Hneut
+  induction Hneut <;> intro t' step
+  · case bvar n =>
+      cases step
+  · case fvar x =>
+      cases step
+  · case app IH Hneut =>
+      cases step <;> try aesop
+      · contradiction
+      constructor
+      · assumption
+      · apply sn_step <;> assumption
+
+@[aesop safe]
+lemma neutral_mst {t t' : Term Var} :
+  neutral t → t ↠βᶠ t' → neutral t' := by
+  intro Hneut h_red
+  induction h_red <;> aesop
+
+lemma neutral_sn {t : Term Var} (Hneut : neutral t) : SN t := by
+  induction Hneut
+  · case bvar n => constructor; intro t' hstep; cases hstep
+  · case fvar x => constructor; intro t' hstep; cases hstep
+  · case app t1 t'_neut t1_sn t1'_sn =>
+      apply sn_app <;> try assumption
+      intro t1' t2' hstep1 hstep2
+      have H_neut := neutral_mst t'_neut hstep1
+      contradiction
+
+lemma abs_sn : ∀ {M N : Term Var},
+  SN (M ^ N) → LC N → SN (Term.abs M) := by
+  intro M N sn_M lc_N
+  generalize h : (M ^ N) = M_open at sn_M
+  revert N M
+  induction sn_M with
+  | sn M_open h_sn ih =>
+      intro M N lc_N h
+      constructor
+      intro M' h_step
+      cases h_step with
+      | @abs h_M_red M' L H =>
+        specialize ih (M' ^ N)
+        rw[←h] at ih
+        apply ih
+        · apply FullBeta.step_open_cong1 <;> assumption
+        · assumption
+        · rfl
+
+
+
+
+lemma multiApp_sn : ∀ {Ps} {M N : Term Var},
+  SN N →
+  SN (multiApp (M ^ N) Ps) →
+  LC N →
+  LC (multiApp (M ^ N) Ps) →
+  -------------------------------------
+  SN (multiApp ((Term.abs M).app N) Ps) := by
+  intro P
+  induction P <;> intros M N sn_N sn_MNPs lc_N lc_MNPs
+  · case nil =>
+      apply sn_app
+      · apply abs_sn at sn_MNPs
+        simp_all
+      · assumption
+      · intro M' N' hstep1 hstep2
+        have Hmst : (M ^ N) ↠βᶠ (M' ^ N') := by
+          apply FullBeta.steps_open_cong_abs <;> try assumption
+          apply open_abs_lc <;> assumption
+        apply sn_mst <;> assumption
+  · case cons P Ps ih =>
+      apply sn_app
+      · apply ih <;> try assumption
+        · apply sn_app_left at sn_MNPs <;> try grind[Untyped.Term.multiApp_lc]
+        · grind[Untyped.Term.multiApp_lc]
+      · apply sn_app_right at sn_MNPs
+        · assumption
+        · cases lc_MNPs
+          assumption
+      · intro Q' P' hstep1 hstep2
+        match (Term.invert_multiApp_mst hstep1) with
+        | ⟨ M', N', Ps', h_M_red, h_N_red, h_Ps_red, h_cases ⟩ =>
+          match h_cases with
+          | Or.inl h_P => cases Ps' <;> rw[multiApp] at h_cases <;> contradiction
+          | Or.inr ⟨ h_st1, h_st2 ⟩ =>
+            have H1 : (multiApp (M ^ N) Ps).app P ↠βᶠ Q' ^ P' := by
+              have H2 : (multiApp (M ^ N) Ps) ↠βᶠ (M' ^ N').multiApp Ps' := by
+                transitivity
+                · apply steps_multiApp_r
+                  · assumption
+                  · rw[multiApp_lc] at lc_MNPs
+                    simp_all
+                · apply steps_multiApp_l
+                  · rw[multiApp_lc] at lc_MNPs
+                    apply FullBeta.steps_open_cong_abs M M' N N' <;> try assumption
+                    · apply open_abs_lc
+                      · apply lc_MNPs.1
+                  · rw[multiApp_lc] at lc_MNPs
+                    apply multiApp_steps_lc at h_Ps_red
+                    simp_all
+              have H3 : (multiApp (M ^ N) Ps) ↠βᶠ Q'.abs := by
+                transitivity <;> try assumption
+              have H4 : Q'.abs.app P' ↠βᶠ Q' ^ P' := by
+                grind[FullBeta.beta, FullBeta.steps_lc]
+              have H4 : ((M ^ N).multiApp Ps).app P ↠βᶠ Q'.abs.app P' := by
+                cases lc_MNPs
+                transitivity
+                · apply FullBeta.redex_app_r_cong <;> assumption
+                · apply FullBeta.redex_app_l_cong <;> grind[FullBeta.step_lc_r]
+              transitivity <;> try assumption
+            apply sn_mst <;> try assumption
+
+
+end LambdaCalculus.LocallyNameless.Untyped.Term
+
+end Cslib

From 055bd9e28b9d0fd58c9be876f324deb44745a005 Mon Sep 17 00:00:00 2001
From: David Wegmann <david.wegmann@fau.de>
Date: Fri, 6 Mar 2026 04:52:26 +0100
Subject: [PATCH 02/22] removed files that do not belong in this pull request

---
 .../LocallyNameless/Stlc/StrongNorm.lean      | 175 ------------------
 1 file changed, 175 deletions(-)
 delete mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
deleted file mode 100644
index ba3db50f6..000000000
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
+++ /dev/null
@@ -1,175 +0,0 @@
-module
-
-import Cslib.Foundations.Data.Relation
-import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
-import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
-import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
-import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
-import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
-
-namespace Cslib
-
-universe u v
-
-namespace LambdaCalculus.LocallyNameless.Stlc
-
-open Untyped Typing LambdaCalculus.LocallyNameless.Untyped.Term
-
-variable {Var : Type u} {Base : Type v} [DecidableEq Var] [HasFresh Var]
-
-open LambdaCalculus.LocallyNameless.Stlc
-open scoped Term
-
-
-
-inductive saturated (S : Set (Term Var)) : Prop :=
-| intro : (∀ M ∈ S, LC M) →
-          (∀ M ∈ S, SN M) →
-          (∀ M, neutral M → LC M → M ∈ S) →
-          (∀ M N P, LC N → SN N → multiApp (M ^ N) P ∈ S → multiApp ((Term.abs M).app N) P ∈ S) →
-          saturated S
-
-
-@[simp]
-def semanticMap (τ : Ty Base) : Set (Term Var) :=
-  match τ with
-  | Ty.base _ => { t : Term Var | SN t ∧ LC t }
-  | Ty.arrow τ₁ τ₂ =>
-    { t : Term Var | ∀ s : Term Var, s ∈ semanticMap τ₁ → (Term.app t s) ∈ semanticMap τ₂ }
-
-
-
-def semanticMap_saturated (τ : Ty Base) :
-    @saturated Var (semanticMap τ) := by
-  induction τ
-  · case base b =>
-      constructor
-      · simp_all
-      · simp_all
-      · simp_all[neutral_sn]
-      · intro M N P lc_N sn_N h_app
-        constructor
-        · simp_all[multiApp_sn]
-        · have H := h_app.2
-          rw[multiApp_lc] at *
-          grind[open_abs_lc]
-  · case arrow τ₁ τ₂ ih₁ ih₂ =>
-      constructor
-      · intro M hM
-        have H := ih₁.3 (.fvar (fresh {})) (.fvar (fresh {})) (.fvar (fresh {}))
-        specialize (hM (fvar (fresh {})) H)
-        apply (ih₂.1) at hM
-        cases hM
-        assumption
-      · intro M hM
-        apply sn_app_left M (Term.fvar (fresh {}))
-        · constructor
-        · have H := ih₁.3 (.fvar (fresh {})) (.fvar (fresh {})) (.fvar (fresh {}))
-          specialize (hM (fvar (fresh {})) H)
-          apply ih₂.2 ; assumption
-      · intro M hneut mlc s hs
-        apply ih₂.3
-        · constructor
-          · assumption
-          · apply ih₁.2
-            assumption
-        · constructor
-          · assumption
-          · apply ih₁.1
-            assumption
-      · intro M N P lc_N sn_N h_app s hs
-        apply ih₂.4 M N (s::P)
-        · apply lc_N
-        · apply sn_N
-        · apply h_app
-          assumption
-
-
-
-
-
-def entails_context (Ns : Term.Environment Var) (Γ : Context Var (Ty Base)) :=
-  ∀ {x τ}, ⟨ x, τ ⟩ ∈ Γ → (multiSubst Ns (Term.fvar x)) ∈ semanticMap τ
-
-lemma entails_context_empty {Γ : Context Var (Ty Base)} :
-  entails_context [] Γ := by
-  intro x τ h_mem
-  rw[multiSubst]
-  apply (semanticMap_saturated τ).3 <;> constructor
-
-
-lemma entails_context_cons (Ns : Term.Environment Var) (Γ : Context Var (Ty Base))
-  (x : Var) (τ : Ty Base) (sub : Term Var) :
-  x ∉ Ns.dom ∪ Ns.fv ∪ Γ.dom →
-  sub ∈ semanticMap τ →
-  entails_context Ns Γ → entails_context (⟨ x, sub ⟩ :: Ns) (⟨ x, τ ⟩ :: Γ) := by
-  intro h_fresh h_mem h_entails y σ h_mem
-  rw[multiSubst]
-  rw[entails_context] at h_entails
-  cases h_mem
-  · case head =>
-    rw[multiSubst_fvar_fresh]
-    · rw[subst_fvar]
-      simp_all
-    · simp_all
-  · case tail h_mem =>
-    specialize (h_entails h_mem)
-    rw [subst_fresh]
-    · assumption
-    · apply multiSubst_preserves_not_fvar
-      apply List.mem_keys_of_mem at h_mem
-      aesop
-
-
-def entails (Γ : Context Var (Ty Base)) (t : Term Var) (τ : Ty Base) :=
-  ∀ Ns, env_LC Ns → (entails_context Ns Γ) → (multiSubst Ns t) ∈ semanticMap τ
-
-
-theorem soundness {Γ : Context Var (Ty Base)} {t : Term Var} {τ : Ty Base} :
-  Γ ⊢ t ∶ τ → entails Γ t τ := by
-  intro derivation_t
-  induction derivation_t
-  · case var Γ xσ_mem_Γ =>
-      intro Ns lc_Ns hsat
-      apply hsat xσ_mem_Γ
-  · case' abs σ Γ t τ L IH derivation_t =>
-      intro Ns lc_Ns hsat s hsat_s
-      rw[multiSubst_abs]
-      apply (semanticMap_saturated _).4 _ _ []
-      · apply (semanticMap_saturated _).1
-        assumption
-      · apply (semanticMap_saturated _).2
-        assumption
-      · rw[multiApp]
-        set x := fresh (t.fv ∪ L ∪ Ns.dom ∪ Ns.fv ∪ Context.dom Γ ∪ (multiSubst Ns t).fv)
-        have hfresh : x ∉ t.fv ∪ L ∪ Ns.dom ∪ Ns.fv ∪ Context.dom Γ  ∪ (multiSubst Ns t).fv := by apply fresh_notMem
-        have hfreshL : x ∉ L := by simp_all
-        have H1 := derivation_t x hfreshL
-        rw[entails] at H1
-        specialize H1 (⟨x,s⟩ :: Ns)
-        rw [multiSubst, multiSubst_open_var, ←subst_intro] at H1
-        · apply H1
-          · apply env_LC_cons
-            · apply (semanticMap_saturated _).1
-              assumption
-            · assumption
-          · apply entails_context_cons <;> simp_all
-        · simp_all
-        · apply (semanticMap_saturated σ).1
-          assumption
-        · simp_all
-        · aesop
-  · case app derivation_t derivation_t' IH IH' =>
-      intro Ns lc_Ns hsat
-      rw[multiSubst_app]
-      apply IH Ns lc_Ns hsat
-      apply IH' Ns lc_Ns hsat
-
-theorem strong_norm {Γ} {t : Term Var} {τ : Ty Base} (der : Γ ⊢ t ∶ τ) : SN t := by
-  have H := soundness der [] (by aesop) entails_context_empty
-  apply (semanticMap_saturated τ).2
-  assumption
-
-end LambdaCalculus.LocallyNameless.Stlc
-
-end Cslib

From c245bbcf87d5bf36bbe89a1fbcb361387e6403ea Mon Sep 17 00:00:00 2001
From: David Wegmann <david.wegmann@fau.de>
Date: Fri, 6 Mar 2026 04:52:47 +0100
Subject: [PATCH 03/22] removed files that do not belong in this pull request

---
 .../LocallyNameless/Untyped/MultiSubst.lean   | 130 -----------
 .../LocallyNameless/Untyped/StrongNorm.lean   | 216 ------------------
 2 files changed, 346 deletions(-)
 delete mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean
 delete mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean
deleted file mode 100644
index 6693f6d53..000000000
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean
+++ /dev/null
@@ -1,130 +0,0 @@
-module
-
-public import Cslib.Foundations.Data.Relation
-public import Cslib.Foundations.Data.HasFresh
-public import Cslib.Foundations.Syntax.HasSubstitution
-public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
-public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
-public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
-
-
-@[expose] public section
-
-namespace Cslib
-
-universe u v
-
-
-namespace LambdaCalculus.LocallyNameless.Untyped.Term
-
-variable {Var : Type u} {Base : Type v} [DecidableEq Var] [HasFresh Var]
-
-
-abbrev Environment (Var : Type u) := Context Var (Term Var)
-
-def multiSubst (σ : Environment Var) (M : Term Var) : Term Var :=
-  match σ with
-  | [] => M
-  | ⟨ i, sub ⟩ :: σ' => (multiSubst σ' M) [ i := sub ]
-
-def Environment.fv (Ns : Environment Var) : Finset Var :=
-  match Ns with
-  | [] => {}
-  | ⟨ _, sub ⟩ :: Ns' => sub.fv ∪ fv Ns'
-
-
-@[simp]
-def env_LC (Γ : Environment Var) : Prop :=
-  ∀ {x M}, ⟨ x, M ⟩ ∈ Γ → LC M
-
-lemma env_LC_cons {Γ : Environment Var} {x : Var} {sub : Term Var}
-  (lc_sub : LC sub)
-  (lc_Γ : env_LC Γ)
-  : env_LC (⟨ x, sub ⟩ :: Γ) := by
-  intro y M h_mem
-  cases h_mem <;> aesop
-
-
-
-def multiSubst_fvar_fresh (Ns : Environment Var) :
-  ∀ x ∉ Ns.dom, multiSubst Ns (Term.fvar x) = Term.fvar x := by
-  induction Ns <;> intro x h_fresh
-  · case nil =>
-      simp [multiSubst]
-  · case cons N Ns ih =>
-      simp only [multiSubst]
-      simp only [Context.dom] at h_fresh
-      rw[ih]
-      · rw[subst_fvar]
-        by_cases h : N.1 = x <;> simp_all
-      · simp_all
-
-lemma multiSubst_preserves_not_fvar {x : Var}
-  (M : Term Var)
-  (Ns : Environment Var)
-  (nmem : x ∉ M.fv ∪ Ns.fv) :
-  x ∉ (multiSubst Ns M).fv := by
-  induction Ns
-  · case nil =>
-      rw[multiSubst]
-      simp_all
-  · case cons N Ns ih =>
-      rw[multiSubst]
-      apply subst_preserve_not_fvar
-      rw[Environment.fv] at nmem
-      simp_all
-
-def multiSubst_app (M N : Term Var) (Ps : Environment Var) :
-        multiSubst Ps (Term.app M N) = Term.app (multiSubst Ps M) (multiSubst Ps N) := by
-  induction Ps
-  · rfl
-  · case cons N Ns ih => rw[multiSubst, multiSubst, ih]; rfl
-
-def multiSubst_abs (M : Term Var) (Ns : Environment Var) :
-    multiSubst Ns (Term.abs M) =
-    Term.abs (multiSubst Ns M) := by
-  induction Ns
-  · rfl
-  · case cons N Ns ih => rw[multiSubst, ih]; rfl
-
-lemma open'_fvar_subst (M N : Term Var) (x : Var) (H : x ∉ Term.fv M) :
-  (i : Nat) → (M ⟦ i ↝ Term.fvar x ⟧) [x := N] = M ⟦ i ↝ N ⟧ := by
-  induction M <;> intro i
-  · case bvar j =>
-      rw[Term.openRec_bvar, Term.openRec_bvar]
-      by_cases h : i = j <;> simp[h, Term.subst_fvar, Term.subst_bvar]
-  · case fvar y =>
-      rw[Term.openRec_fvar, Term.openRec_fvar]
-      simp only [Term.fv, Finset.mem_singleton] at H
-      simp only [subst_fvar, ite_eq_right_iff]
-      intro H
-      contradiction
-  · case abs M ih =>
-      rw[Term.openRec_abs, Term.openRec_abs]
-      rw[Term.subst_abs]
-      rw[ih H]
-  · case app l r ih_l ih_r =>
-      rw[Term.openRec_app, Term.openRec_app]
-      rw[Term.subst_app]
-      simp only [Term.fv, Finset.mem_union, not_or] at H
-      rw[ih_l H.1]
-      rw[ih_r H.2]
-
-lemma multiSubst_open_var (M : Term Var) (Ns : Environment Var) (x : Var) :
-  x ∉ Ns.dom →
-  env_LC Ns →
-  (multiSubst Ns (M ^ (Term.fvar x))) =
-  (multiSubst Ns M) ^ (Term.fvar x) := by
-  intro h_ndom h_lc
-  induction Ns with
-  | nil => rfl
-  | cons N Ns ih =>
-    rw[multiSubst, multiSubst]
-    rw[ih]
-    · rw[subst_open_var] <;> aesop
-    · simp_all
-    aesop
-
-end LambdaCalculus.LocallyNameless.Untyped.Term
-
-end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
deleted file mode 100644
index 01f673c1d..000000000
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
+++ /dev/null
@@ -1,216 +0,0 @@
-module
-
-public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
-public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
-public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
-
-@[expose] public section
-
-namespace Cslib
-
-universe u
-
-variable {Var : Type u} [DecidableEq Var] [HasFresh Var]
-
-
-namespace LambdaCalculus.LocallyNameless.Untyped.Term
-
-attribute [grind =] Finset.union_singleton
-
-
-inductive SN {α} : Term α → Prop
-| sn t : (∀ (t' : Term α), (t ⭢βᶠ t') → SN t') → SN t
-
-@[aesop safe]
-lemma sn_step {t t' : Term Var} (t_st_t' : t ⭢βᶠ t') (sn_t : SN t) : SN t' := by
-  cases sn_t; grind
-
-@[aesop safe]
-lemma sn_mst {t t' : Term Var} (t_st_t' : t ↠βᶠ t') (sn_t : SN t) : SN t' := by
-  induction t_st_t' <;> grind[sn_step]
-
-lemma sn_fvar {x : Var} : SN (Term.fvar x) := by
-  constructor
-  intro t' hstep
-  cases hstep
-
-lemma sn_app (t s : Term Var) :
-  SN t →
-  SN s →
-  (∀ {t' s' : Term Var}, t ↠βᶠ t'.abs → s ↠βᶠ s' → SN (t' ^ s')) →
-  SN (t.app s) := by
-  intro h_sn_t h_sn_s hβ
-  induction h_sn_t generalizing s with | sn t ht ih_t =>
-  induction h_sn_s with | sn s hs ih_s =>
-  constructor
-  intro u hstep
-  cases hstep with
-  | beta _ _ => apply hβ <;> rfl
-  | appL _ h_s_red =>
-    apply ih_s _ h_s_red
-    intro t' s'' hstep1 hstep2
-    exact hβ hstep1 (Relation.ReflTransGen.head h_s_red hstep2)
-  | appR _ h_t_red =>
-    apply ih_t _ h_t_red _ (SN.sn s hs)
-    intro t' s' hstep1 hstep2
-    exact hβ (Relation.ReflTransGen.head h_t_red hstep1) hstep2
-
-
-
-lemma sn_app_left (M N : Term Var) : Term.LC N → SN (M.app N) → SN M := by
-  intro lc_N h_sn
-  generalize Heq : M.app N = P
-  rw[Heq] at h_sn
-  revert M N
-  induction h_sn
-  · case sn P h_sn ih =>
-    intro M N lc_N Heq
-    rw[←Heq] at ih
-    constructor
-    intro M' h_step
-    apply ih (M'.app N)
-    apply Term.FullBeta.appR <;> assumption
-    · assumption
-    · rfl
-
-lemma sn_app_right (M N : Term Var) : Term.LC M → SN (M.app N) → SN N := by
-  intro lc_N h_sn
-  generalize Heq : M.app N = P
-  rw[Heq] at h_sn
-  revert M N
-  induction h_sn
-  · case sn P h_sn ih =>
-    intro M N lc_N Heq
-    rw[←Heq] at ih
-    constructor
-    intro N' h_step
-    apply ih (M.app N')
-    apply Term.FullBeta.appL <;> assumption
-    · assumption
-    · rfl
-
-@[aesop safe constructors]
-inductive neutral : Term Var → Prop
-| bvar : ∀ n, neutral (Term.bvar n)
-| fvar : ∀ x, neutral (Term.fvar x)
-| app : ∀ t1 t2, neutral t1 → SN t2 → neutral (Term.app t1 t2)
-
-@[aesop safe]
-lemma neutral_step {t : Term Var} :
-  neutral t → ∀ t', t ⭢βᶠ t' → neutral t' := by
-  intro Hneut
-  induction Hneut <;> intro t' step
-  · case bvar n =>
-      cases step
-  · case fvar x =>
-      cases step
-  · case app IH Hneut =>
-      cases step <;> try aesop
-      · contradiction
-      constructor
-      · assumption
-      · apply sn_step <;> assumption
-
-@[aesop safe]
-lemma neutral_mst {t t' : Term Var} :
-  neutral t → t ↠βᶠ t' → neutral t' := by
-  intro Hneut h_red
-  induction h_red <;> aesop
-
-lemma neutral_sn {t : Term Var} (Hneut : neutral t) : SN t := by
-  induction Hneut
-  · case bvar n => constructor; intro t' hstep; cases hstep
-  · case fvar x => constructor; intro t' hstep; cases hstep
-  · case app t1 t'_neut t1_sn t1'_sn =>
-      apply sn_app <;> try assumption
-      intro t1' t2' hstep1 hstep2
-      have H_neut := neutral_mst t'_neut hstep1
-      contradiction
-
-lemma abs_sn : ∀ {M N : Term Var},
-  SN (M ^ N) → LC N → SN (Term.abs M) := by
-  intro M N sn_M lc_N
-  generalize h : (M ^ N) = M_open at sn_M
-  revert N M
-  induction sn_M with
-  | sn M_open h_sn ih =>
-      intro M N lc_N h
-      constructor
-      intro M' h_step
-      cases h_step with
-      | @abs h_M_red M' L H =>
-        specialize ih (M' ^ N)
-        rw[←h] at ih
-        apply ih
-        · apply FullBeta.step_open_cong1 <;> assumption
-        · assumption
-        · rfl
-
-
-
-
-lemma multiApp_sn : ∀ {Ps} {M N : Term Var},
-  SN N →
-  SN (multiApp (M ^ N) Ps) →
-  LC N →
-  LC (multiApp (M ^ N) Ps) →
-  -------------------------------------
-  SN (multiApp ((Term.abs M).app N) Ps) := by
-  intro P
-  induction P <;> intros M N sn_N sn_MNPs lc_N lc_MNPs
-  · case nil =>
-      apply sn_app
-      · apply abs_sn at sn_MNPs
-        simp_all
-      · assumption
-      · intro M' N' hstep1 hstep2
-        have Hmst : (M ^ N) ↠βᶠ (M' ^ N') := by
-          apply FullBeta.steps_open_cong_abs <;> try assumption
-          apply open_abs_lc <;> assumption
-        apply sn_mst <;> assumption
-  · case cons P Ps ih =>
-      apply sn_app
-      · apply ih <;> try assumption
-        · apply sn_app_left at sn_MNPs <;> try grind[Untyped.Term.multiApp_lc]
-        · grind[Untyped.Term.multiApp_lc]
-      · apply sn_app_right at sn_MNPs
-        · assumption
-        · cases lc_MNPs
-          assumption
-      · intro Q' P' hstep1 hstep2
-        match (Term.invert_multiApp_mst hstep1) with
-        | ⟨ M', N', Ps', h_M_red, h_N_red, h_Ps_red, h_cases ⟩ =>
-          match h_cases with
-          | Or.inl h_P => cases Ps' <;> rw[multiApp] at h_cases <;> contradiction
-          | Or.inr ⟨ h_st1, h_st2 ⟩ =>
-            have H1 : (multiApp (M ^ N) Ps).app P ↠βᶠ Q' ^ P' := by
-              have H2 : (multiApp (M ^ N) Ps) ↠βᶠ (M' ^ N').multiApp Ps' := by
-                transitivity
-                · apply steps_multiApp_r
-                  · assumption
-                  · rw[multiApp_lc] at lc_MNPs
-                    simp_all
-                · apply steps_multiApp_l
-                  · rw[multiApp_lc] at lc_MNPs
-                    apply FullBeta.steps_open_cong_abs M M' N N' <;> try assumption
-                    · apply open_abs_lc
-                      · apply lc_MNPs.1
-                  · rw[multiApp_lc] at lc_MNPs
-                    apply multiApp_steps_lc at h_Ps_red
-                    simp_all
-              have H3 : (multiApp (M ^ N) Ps) ↠βᶠ Q'.abs := by
-                transitivity <;> try assumption
-              have H4 : Q'.abs.app P' ↠βᶠ Q' ^ P' := by
-                grind[FullBeta.beta, FullBeta.steps_lc]
-              have H4 : ((M ^ N).multiApp Ps).app P ↠βᶠ Q'.abs.app P' := by
-                cases lc_MNPs
-                transitivity
-                · apply FullBeta.redex_app_r_cong <;> assumption
-                · apply FullBeta.redex_app_l_cong <;> grind[FullBeta.step_lc_r]
-              transitivity <;> try assumption
-            apply sn_mst <;> try assumption
-
-
-end LambdaCalculus.LocallyNameless.Untyped.Term
-
-end Cslib

From c9c2236348810570b445368e0d42c1ed1ab3b954 Mon Sep 17 00:00:00 2001
From: David Wegmann <david.wegmann@fau.de>
Date: Sat, 7 Mar 2026 03:29:26 +0100
Subject: [PATCH 04/22] applied the same style suggestions from the previous
 pull request

---
 .../LocallyNameless/Untyped/MultiApp.lean     | 134 ++++++++++++------
 1 file changed, 90 insertions(+), 44 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 312b8a6c8..8a9d832bf 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -1,3 +1,7 @@
+/-
+Author: David Wegmann
+-/
+
 module
 
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
@@ -12,12 +16,24 @@ variable {Var : Type u} [DecidableEq Var] [HasFresh Var]
 
 namespace LambdaCalculus.LocallyNameless.Untyped.Term
 
+
+/-
+  multiApp f [x_1, x_2, ..., x_n] applies the arguments x_1, x_2, ..., x_n
+  to f in left-associative order, i.e. as (((f x_1) x_2) ... x_n).
+-/
 @[simp]
 def multiApp (f : Term Var) (args : List (Term Var)) :=
   match args with
   | []      => f
   | a :: as => Term.app (multiApp f as) a
 
+/-
+  A list of arguments performs a single reduction step
+
+  [x_1, ..., x_i ..., x_n] ⭢βᶠ [x_1, ..., x_i', ..., x_n]
+
+  if one of the arguments performs a single step, and the rest are locally closed.
+-/
 @[reduction_sys "βᶠ"]
 inductive multiApp_full_beta : List (Term Var) → List (Term Var) → Prop where
 | step : N ⭢βᶠ N' → (∀ N ∈ Ns, LC N) → multiApp_full_beta (N :: Ns) (N' :: Ns)
@@ -25,66 +41,82 @@ inductive multiApp_full_beta : List (Term Var) → List (Term Var) → Prop wher
 
 attribute [scoped grind .] multiApp_full_beta.step multiApp_full_beta.cons
 
+/- just like ordinary beta reduction, the right-hand side
+   of a multi-application step is locally closed -/
 lemma multiApp_step_lc_r {Ns Ns' : List (Term Var)}
-  (step : Ns ⭢βᶠ Ns')
-  : (∀ N ∈ Ns', LC N) := by
-  induction step <;> grind[FullBeta.step_lc_r]
+  (step : Ns ⭢βᶠ Ns') :
+    (∀ N ∈ Ns', LC N) := by
+  induction step <;> grind [FullBeta.step_lc_r]
 
+/- just like ordinary beta reduction, multiple steps of a argument list preserves local closure -/
 lemma multiApp_steps_lc {Ns Ns' : List (Term Var)}
-  (step : Ns ↠βᶠ Ns') (H : ∀ N ∈ Ns, LC N)
-  : (∀ N ∈ Ns', LC N) := by
-  induction step <;> grind[FullBeta.step_lc_r, multiApp_step_lc_r]
+  (step : Ns ↠βᶠ Ns') (H : ∀ N ∈ Ns, LC N) :
+    (∀ N ∈ Ns', LC N) := by
+  induction step <;> grind [FullBeta.step_lc_r, multiApp_step_lc_r]
 
+/- a term resulting from a multi-application is locally closed if
+   and only if the leftmost term and all arguments applied to it are locally closed -/
 @[scoped grind ←]
 lemma multiApp_lc {M : Term Var} {Ns : List (Term Var)} :
-  LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N)
+    LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N)
    := by
   constructor
   · induction Ns
-    · case nil => grind[multiApp]
+    · case nil => grind [multiApp]
     · case cons N Ns ih => intro h_lc; cases h_lc; grind
-  · induction Ns <;> grind[multiApp, LC.app]
+  · induction Ns <;> grind [multiApp, LC.app]
 
+/- just like ordinary beta reduction, the left-hand side
+   of a multi-application step is locally closed -/
 @[scoped grind ←]
-lemma step_multiApp_l {M M' : Term Var} {Ns : List (Term Var)} :
-  M ⭢βᶠ M' →
-  (∀ N ∈ Ns, LC N) →
-  M.multiApp Ns ⭢βᶠ M'.multiApp Ns := by
-  induction Ns <;> grind[multiApp, FullBeta.appR]
+lemma step_multiApp_l {M M' : Term Var} {Ns : List (Term Var)}
+  (steps : M ⭢βᶠ M')
+  (lc_Ns : ∀ N ∈ Ns, LC N) :
+    M.multiApp Ns ⭢βᶠ M'.multiApp Ns := by
+  induction Ns <;> grind [multiApp, FullBeta.appR]
 
+/- congruence lemma for multi reduction of the left most term of a multi-application -/
 @[scoped grind ←]
 lemma steps_multiApp_l {M M' : Term Var} {Ns : List (Term Var)}
   (steps : M ↠βᶠ M')
-  (lc_Ns : ∀ N ∈ Ns, LC N)
-  : M.multiApp Ns ↠βᶠ M'.multiApp Ns := by
+  (lc_Ns : ∀ N ∈ Ns, LC N) :
+    M.multiApp Ns ↠βᶠ M'.multiApp Ns := by
   induction steps <;> grind
 
+/- congruence lemma for single reduction of one of the arguments of a multi-application -/
 @[scoped grind ←]
 lemma step_multiApp_r {M : Term Var} {Ns Ns' : List (Term Var)}
   (steps : Ns ⭢βᶠ Ns')
-  (lc_M : LC M)
-  : M.multiApp Ns ⭢βᶠ M.multiApp Ns' := by
-  induction steps <;> grind[multiApp,FullBeta.appL,FullBeta.appR]
+  (lc_M : LC M) :
+    M.multiApp Ns ⭢βᶠ M.multiApp Ns' := by
+  induction steps <;> grind [multiApp, FullBeta.appL, FullBeta.appR]
 
+/- congruence lemma for multiple reduction of one of the arguments of a multi-application -/
 @[scoped grind ←]
 lemma steps_multiApp_r {M : Term Var} {Ns Ns' : List (Term Var)}
   (steps : Ns ↠βᶠ Ns')
-  (lc_M : LC M)
-  : M.multiApp Ns ↠βᶠ M.multiApp Ns' := by
-  induction steps <;> grind[multiApp,FullBeta.appL,FullBeta.appR]
-
-lemma invert_multiApp_st {Ps} {M N Q : Term Var}
+  (lc_M : LC M) :
+    M.multiApp Ns ↠βᶠ M.multiApp Ns' := by
+  induction steps <;> grind [multiApp, FullBeta.appL, FullBeta.appR]
+
+/- if a term (λ M) N P_1 ... P_n reduces in a single step to Q, then
+   Q must be one of the following forms:
+
+    Q = (λ M') N P_1 ... P_n where M ⭢βᶠ M' or
+    Q = (λ M) N' P_1 ... P_n where N ⭢βᶠ N' or
+    Q = (λ M) N P_1' ... P_n' where P_i ⭢βᶠ P_i' for some i or
+    Q = (M ^ N) P_1 ... P_n
+-/
+lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
   (h_red : multiApp (M.abs.app N) Ps ⭢βᶠ Q) :
-  (∃ M', M.abs ⭢βᶠ Term.abs M' ∧ Q = multiApp (M'.abs.app N) Ps) ∨
-  (∃ N', N ⭢βᶠ N' ∧ Q = multiApp (M.abs.app N') Ps) ∨
-  (∃ Ps', Ps ⭢βᶠ Ps' ∧ Q = multiApp (M.abs.app N) Ps') ∨
-  (Q = multiApp (M ^ N) Ps) := by
-  revert M N Q h_red
-  induction Ps with
+    (∃ M', M.abs ⭢βᶠ Term.abs M' ∧ Q = multiApp (M'.abs.app N) Ps) ∨
+    (∃ N', N ⭢βᶠ N' ∧ Q = multiApp (M.abs.app N') Ps) ∨
+    (∃ Ps', Ps ⭢βᶠ Ps' ∧ Q = multiApp (M.abs.app N) Ps') ∨
+    (Q = multiApp (M ^ N) Ps) := by
+  induction Ps generalizing M N Q with
   | nil =>
-    intro N N P h_red
-    rw[multiApp] at h_red
-    rw[multiApp]
+    rw [multiApp] at h_red
+    rw [multiApp]
     cases h_red
     · case beta abs_lc n_lc => aesop
     · case appL M N' lc_z h_red => aesop
@@ -98,11 +130,10 @@ lemma invert_multiApp_st {Ps} {M N Q : Term Var}
               assumption
             · rfl
   | cons P Ps ih =>
-    intro M N Q h_red
     have h_lc := (FullBeta.step_lc_l h_red)
     rw [multiApp] at h_red
     generalize Heq : (M.abs.app N).multiApp Ps = Q'
-    rw[Heq] at h_red
+    rw [Heq] at h_red
     cases h_red
     · case beta abs_lc n_lc => cases Ps <;> contradiction
     · case appL Y M P' lc_z h_red =>
@@ -111,7 +142,7 @@ lemma invert_multiApp_st {Ps} {M N Q : Term Var}
         simp
         grind
     · case appR M Q'' h_red P_lc =>
-        rw[←Heq] at h_red
+        rw [←Heq] at h_red
         match (ih h_red) with
         | .inl ⟨ M', st, Heq' ⟩                => aesop
         | .inr (.inl ⟨ N', st, Heq' ⟩)         => aesop
@@ -122,13 +153,28 @@ lemma invert_multiApp_st {Ps} {M N Q : Term Var}
           grind
         | .inr (.inr (.inr Heq'))              => aesop
 
+/- if a term (λ M) N P_1 ... P_n reduces in multiple steps to Q, then either Q if of the form
+
+    Q = (λ M') N' P'_1 ... P'_n
+
+   or
+
+    we first reach an intermediate term of this shape,
+
+    (λ M) N P_1 ... P_n ↠βᶠ (λ M') N' P'_1 ... P'_n
+
+    then perform a beta reduction and reduce further to Q
+
+    (λ M') N' P'_1 ... P'_n ↠βᶠ M' ^ N' P'_1 ... P'_n ↠βᶠ Q
 
-lemma invert_multiApp_mst {Ps} {M N Q : Term Var}
+   where M ↠βᶠ M' and N ↠βᶠ N' and P_i ↠βᶠ P_i' for all i,
+-/
+lemma invert_abs_multiApp_mst {Ps} {M N Q : Term Var}
   (h_red : multiApp (M.abs.app N) Ps ↠βᶠ Q) :
-  ∃ M' N' Ns', M.abs ↠βᶠ M'.abs ∧ N ↠βᶠ N' ∧ Ps ↠βᶠ Ns' ∧
-    (Q = multiApp (M'.abs.app N') Ns' ∨
-     (multiApp (M.abs.app N) Ps ↠βᶠ multiApp (M'^ N') Ns' ∧
-                                      multiApp (M'^ N') Ns' ↠βᶠ Q)) := by
+    ∃ M' N' Ns', M.abs ↠βᶠ M'.abs ∧ N ↠βᶠ N' ∧ Ps ↠βᶠ Ns' ∧
+                 (Q = multiApp (M'.abs.app N') Ns' ∨
+     (multiApp (M.abs.app N) Ps ↠βᶠ multiApp (M' ^ N') Ns' ∧
+                                      multiApp (M' ^ N') Ns' ↠βᶠ Q)) := by
   induction h_red
   · case refl => grind
   · case tail Q' Q'' steps step ih =>
@@ -136,13 +182,13 @@ lemma invert_multiApp_mst {Ps} {M N Q : Term Var}
     | ⟨ M', N', Ps', st_M, st_N, st_Ps, Cases ⟩ =>
       match Cases with
       | .inl Heq =>
-        rw[Heq] at step
-        match (invert_multiApp_st step) with
+        rw [Heq] at step
+        match (invert_abs_multiApp_st step) with
         | .inl ⟨ M'', st, HeqM'' ⟩             => grind
         | .inr (.inl ⟨ N', st, Heq' ⟩)         => grind
         | .inr (.inr (.inl ⟨ Ps', st, Heq' ⟩)) => grind
         | .inr (.inr (.inr Heq'))              => grind
-      | .inr ⟨ steps1, steps2 ⟩ => grind[Relation.ReflTransGen.single]
+      | .inr ⟨ steps1, steps2 ⟩ => grind [Relation.ReflTransGen.single]
 
 end LambdaCalculus.LocallyNameless.Untyped.Term
 

From f21151bbea1a3f0364e97cad978c93df474ebabc Mon Sep 17 00:00:00 2001
From: David Wegmann <david.wegmann@fau.de>
Date: Sat, 7 Mar 2026 03:44:09 +0100
Subject: [PATCH 05/22] removed accidental reversion in LcAt

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
index c85cf3161..092c176c1 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
@@ -86,15 +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 : ℕ) :
+/- Opening for some term at i-th bound variable increments `LcAt` by one -/
+lemma 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
+  induction M generalizing i <;> grind
+
+/- When `M ^ N` is locally closed, then `M.abs` is locally closed. This is proven by translating LC
+   to LcAt, applying lcAt_openRec_lcAt, then translating back to LC -/
+lemma open_abs_lc [HasFresh Var] {M N : Term Var} (hlc : LC (M ^ N)) : LC (M.abs) := by
+  rw [← lcAt_iff_LC] at *
+  exact lcAt_openRec_lcAt _ _ _ hlc
 
 end Cslib.LambdaCalculus.LocallyNameless.Untyped.Term

From 4e09785a99583dfce4d0cd4537692fee29972f89 Mon Sep 17 00:00:00 2001
From: David Wegmann <david.wegmann@fau.de>
Date: Sat, 7 Mar 2026 03:45:46 +0100
Subject: [PATCH 06/22] removed accidental reversion in FullBeta

---
 .../LocallyNameless/Untyped/FullBeta.lean     | 191 ++++++------------
 1 file changed, 63 insertions(+), 128 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
index 2b5c79242..742f000b4 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
@@ -8,7 +8,6 @@ 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
 
@@ -56,8 +55,6 @@ 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
@@ -77,44 +74,21 @@ 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') :
-    s [ x := fvar y ] ⭢βᶠ s' [ x := fvar y ] := by
-  induction step
-  case beta m n abs_lc n_lc =>
-    cases abs_lc with | abs xs _ mem =>
-      rw [subst_open x (fvar y) n m (by grind)]
-      refine beta ?_ (by grind)
-      exact subst_lc (LC.abs xs m mem) (LC.fvar y)
-  case abs => grind [abs <| free_union Var]
-  all_goals grind
-
-/-- Substitution respects a single reduction step. -/
+/-- Substitution of a locally closed term 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
 
+/-- Substitution respects a single reduction step of a free variable. -/
+lemma redex_subst_cong (s s' : Term Var) (x y : Var) (step : s ⭢βᶠ s') :
+    s [ x := fvar y ] ⭢βᶠ s' [ x := fvar y ] :=
+  redex_subst_cong_lc _ _ _ _ step (.fvar y)
 
 /-- 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
@@ -141,106 +115,67 @@ 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]
+/- Reduction is preserved when opening with a locally closed term. -/
+lemma step_open_cong_l
+  (s s' t) (L : Finset Var) (step : ∀ x ∉ L, (s ^ fvar x) ⭢βᶠ (s' ^ fvar x)) (h_lc : LC t) :
+    (s ^ t) ⭢βᶠ (s' ^ t) := by
+  have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
+  grind [subst_intro, redex_subst_cong_lc]
 
+/- Multiple reduction `λ s ↠βᶠ t` implies `t = λ s'` for some s' -/
 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
+    ∃ (s' : Term Var), s.abs ↠βᶠ s'.abs ∧ t = s'.abs := by
+  induction step with
+  | refl => grind
+  | tail _ step _ => cases step with grind [step_abs_cong (free_union Var)]
+
+/- `λ s ↠βᶠ λ s'` implies `s ^ t ↠βᶠ s' ^ t'` -/
+lemma steps_open_cong_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) :
+  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 (L := free_union Var)]
+
+/- `t ↠βᶠ t'` implies `s [ x := t ] ↠βᶠ s [ x := t' ]`.
+   There is no single step lemma in this case because x
+   may be substituted for n times, so a single step t ↠βᶠ t
+   in general requires n steps in `s [ x := t ] ↠βᶠ (s [ x := t' ])` -/
+lemma step_subst_cong_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) :
+  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
+
+/- `step_subst_cong_r` can be generalized to multiple reductions `t ↠βᶠ t'`.
+   This requires s to be locally closed, locally closedness of t and t'
+   can be infered by the fact t reduces to t' -/
+lemma steps_subst_cong_r {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
+  induction step with
+  | refl => rfl
+  | tail steps step ih => grind [Relation.ReflTransGen.trans, step_subst_cong_r]
 
+/- When both `t` and `s` reduce to `t'` and `s'`, then `t ^ s` reduces to `t' ^ s'` -/
 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) :
+  (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]
+  cases lc_s with
+  | abs L =>
+    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_cong_r]
+      · grind [=_ subst_intro, steps_open_cong_l_abs]
+    all_goals grind
 
 end LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta
 

From 58aae9529e6afde3de5229e3650db50c7c5b2f67 Mon Sep 17 00:00:00 2001
From: David Wegmann <david.wegmann@fau.de>
Date: Sat, 7 Mar 2026 03:46:38 +0100
Subject: [PATCH 07/22] removed accidental reversion in Properties

---
 .../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 56dba11609d265cd91cb2267e93b45ca79c75594 Mon Sep 17 00:00:00 2001
From: David Wegmann <david.wegmann@fau.de>
Date: Sat, 7 Mar 2026 03:59:44 +0100
Subject: [PATCH 08/22] instructed linter to ignore warnings

---
 .../LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean    | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 8a9d832bf..5b409a6fc 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -2,10 +2,16 @@
 Author: David Wegmann
 -/
 
+
 module
 
+
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
 
+set_option linter.unusedDecidableInType false
+set_option linter.unusedSectionVars false false
+set_option linter.unusedVariables false
+
 @[expose] public section
 
 namespace Cslib

From 83b6d047127bff9430cb06374457936810fcb901 Mon Sep 17 00:00:00 2001
From: David Wegmann <david.wegmann@fau.de>
Date: Sat, 7 Mar 2026 04:02:35 +0100
Subject: [PATCH 09/22] removed one false too much

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 5b409a6fc..3598637b7 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -9,7 +9,7 @@ module
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
 
 set_option linter.unusedDecidableInType false
-set_option linter.unusedSectionVars false false
+set_option linter.unusedSectionVars false
 set_option linter.unusedVariables false
 
 @[expose] public section

From 107a41916fcd3263a75a225997d6fec6ffd83e7b Mon Sep 17 00:00:00 2001
From: David Wegmann <david.wegmann@fau.de>
Date: Sat, 7 Mar 2026 04:10:51 +0100
Subject: [PATCH 10/22] ran lake exe mk_all

---
 Cslib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Cslib.lean b/Cslib.lean
index a9d5ffc3e..85be92620 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -91,6 +91,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
 public import Cslib.Logics.HML.Basic

From 85a6038ddbee7cb3b0b18dc629eb7894a14c2ab4 Mon Sep 17 00:00:00 2001
From: David Wegmann <david.wegmann@fau.de>
Date: Sat, 7 Mar 2026 22:39:53 +0100
Subject: [PATCH 11/22] implemented some of the requested changed

---
 .../LocallyNameless/Untyped/MultiApp.lean     | 24 ++++++++++++-------
 1 file changed, 15 insertions(+), 9 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 3598637b7..a56652f07 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -1,5 +1,7 @@
 /-
-Author: David Wegmann
+Copyright (c) 2025 David Wegmann. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Wegmann
 -/
 
 
@@ -9,8 +11,6 @@ module
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
 
 set_option linter.unusedDecidableInType false
-set_option linter.unusedSectionVars false
-set_option linter.unusedVariables false
 
 @[expose] public section
 
@@ -36,9 +36,10 @@ def multiApp (f : Term Var) (args : List (Term Var)) :=
 /-
   A list of arguments performs a single reduction step
 
-  [x_1, ..., x_i ..., x_n] ⭢βᶠ [x_1, ..., x_i', ..., x_n]
+  [x₁, ..., xᵢ ..., xₙ] ⭢βᶠ [x₁, ..., xᵢ', ..., xₙ]
 
-  if one of the arguments performs a single step, and the rest are locally closed.
+  if one of the arguments performs a single step xᵢ ⭢βᶠ xᵢ'
+  and the rest of the arguments are locally closed.
 -/
 @[reduction_sys "βᶠ"]
 inductive multiApp_full_beta : List (Term Var) → List (Term Var) → Prop where
@@ -62,6 +63,7 @@ lemma multiApp_steps_lc {Ns Ns' : List (Term Var)}
 
 /- a term resulting from a multi-application is locally closed if
    and only if the leftmost term and all arguments applied to it are locally closed -/
+omit [DecidableEq Var] [HasFresh Var] in
 @[scoped grind ←]
 lemma multiApp_lc {M : Term Var} {Ns : List (Term Var)} :
     LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N)
@@ -74,6 +76,7 @@ lemma multiApp_lc {M : Term Var} {Ns : List (Term Var)} :
 
 /- just like ordinary beta reduction, the left-hand side
    of a multi-application step is locally closed -/
+omit [DecidableEq Var] [HasFresh Var] in
 @[scoped grind ←]
 lemma step_multiApp_l {M M' : Term Var} {Ns : List (Term Var)}
   (steps : M ⭢βᶠ M')
@@ -82,6 +85,7 @@ lemma step_multiApp_l {M M' : Term Var} {Ns : List (Term Var)}
   induction Ns <;> grind [multiApp, FullBeta.appR]
 
 /- congruence lemma for multi reduction of the left most term of a multi-application -/
+omit [DecidableEq Var] [HasFresh Var] in
 @[scoped grind ←]
 lemma steps_multiApp_l {M M' : Term Var} {Ns : List (Term Var)}
   (steps : M ↠βᶠ M')
@@ -90,6 +94,7 @@ lemma steps_multiApp_l {M M' : Term Var} {Ns : List (Term Var)}
   induction steps <;> grind
 
 /- congruence lemma for single reduction of one of the arguments of a multi-application -/
+omit [DecidableEq Var] [HasFresh Var] in
 @[scoped grind ←]
 lemma step_multiApp_r {M : Term Var} {Ns Ns' : List (Term Var)}
   (steps : Ns ⭢βᶠ Ns')
@@ -98,6 +103,7 @@ lemma step_multiApp_r {M : Term Var} {Ns Ns' : List (Term Var)}
   induction steps <;> grind [multiApp, FullBeta.appL, FullBeta.appR]
 
 /- congruence lemma for multiple reduction of one of the arguments of a multi-application -/
+omit [DecidableEq Var] [HasFresh Var] in
 @[scoped grind ←]
 lemma steps_multiApp_r {M : Term Var} {Ns Ns' : List (Term Var)}
   (steps : Ns ↠βᶠ Ns')
@@ -108,10 +114,10 @@ lemma steps_multiApp_r {M : Term Var} {Ns Ns' : List (Term Var)}
 /- if a term (λ M) N P_1 ... P_n reduces in a single step to Q, then
    Q must be one of the following forms:
 
-    Q = (λ M') N P_1 ... P_n where M ⭢βᶠ M' or
-    Q = (λ M) N' P_1 ... P_n where N ⭢βᶠ N' or
-    Q = (λ M) N P_1' ... P_n' where P_i ⭢βᶠ P_i' for some i or
-    Q = (M ^ N) P_1 ... P_n
+    Q = (λ M') N P₁ ... Pₙ where M ⭢βᶠ M' or
+    Q = (λ M) N' P₁ ... Pₙ where N ⭢βᶠ N' or
+    Q = (λ M) N P₁' ... Pₙ' where P_i ⭢βᶠ P_i' for some i or
+    Q = (M ^ N) P₁ ... Pₙ
 -/
 lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
   (h_red : multiApp (M.abs.app N) Ps ⭢βᶠ Q) :

From bedab8a2a1a1548981d51b10ae9117931747bc81 Mon Sep 17 00:00:00 2001
From: David Wegmann <david.wegmann@fau.de>
Date: Sat, 7 Mar 2026 22:57:00 +0100
Subject: [PATCH 12/22] renamed multiApp_full_beta to list_full_beta and added
 l to notation to distinguish between Term and List Term reductions

---
 .../LocallyNameless/Untyped/MultiApp.lean     | 54 +++++++++----------
 1 file changed, 24 insertions(+), 30 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index a56652f07..086c71518 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -27,7 +27,7 @@ namespace LambdaCalculus.LocallyNameless.Untyped.Term
   multiApp f [x_1, x_2, ..., x_n] applies the arguments x_1, x_2, ..., x_n
   to f in left-associative order, i.e. as (((f x_1) x_2) ... x_n).
 -/
-@[simp]
+@[simp, scoped grind =]
 def multiApp (f : Term Var) (args : List (Term Var)) :=
   match args with
   | []      => f
@@ -41,23 +41,22 @@ def multiApp (f : Term Var) (args : List (Term Var)) :=
   if one of the arguments performs a single step xᵢ ⭢βᶠ xᵢ'
   and the rest of the arguments are locally closed.
 -/
-@[reduction_sys "βᶠ"]
-inductive multiApp_full_beta : List (Term Var) → List (Term Var) → Prop where
-| step : N ⭢βᶠ N' → (∀ N ∈ Ns, LC N) → multiApp_full_beta (N :: Ns) (N' :: Ns)
-| cons : LC N → multiApp_full_beta Ns Ns' → multiApp_full_beta (N :: Ns) (N :: Ns')
+@[reduction_sys "lβᶠ"]
+inductive list_full_beta : List (Term Var) → List (Term Var) → Prop where
+| step : N ⭢βᶠ N' → (∀ N ∈ Ns, LC N) → list_full_beta (N :: Ns) (N' :: Ns)
+| cons : LC N → list_full_beta Ns Ns' → list_full_beta (N :: Ns) (N :: Ns')
 
-attribute [scoped grind .] multiApp_full_beta.step multiApp_full_beta.cons
+attribute [scoped grind .] list_full_beta.step list_full_beta.cons
 
 /- just like ordinary beta reduction, the right-hand side
    of a multi-application step is locally closed -/
-lemma multiApp_step_lc_r {Ns Ns' : List (Term Var)}
-  (step : Ns ⭢βᶠ Ns') :
+lemma multiApp_step_lc_r {Ns Ns' : List (Term Var)} (step : Ns ⭢lβᶠ Ns') :
     (∀ N ∈ Ns', LC N) := by
   induction step <;> grind [FullBeta.step_lc_r]
 
 /- just like ordinary beta reduction, multiple steps of a argument list preserves local closure -/
 lemma multiApp_steps_lc {Ns Ns' : List (Term Var)}
-  (step : Ns ↠βᶠ Ns') (H : ∀ N ∈ Ns, LC N) :
+  (step : Ns ↠lβᶠ Ns') (H : ∀ N ∈ Ns, LC N) :
     (∀ N ∈ Ns', LC N) := by
   induction step <;> grind [FullBeta.step_lc_r, multiApp_step_lc_r]
 
@@ -66,12 +65,11 @@ lemma multiApp_steps_lc {Ns Ns' : List (Term Var)}
 omit [DecidableEq Var] [HasFresh Var] in
 @[scoped grind ←]
 lemma multiApp_lc {M : Term Var} {Ns : List (Term Var)} :
-    LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N)
-   := by
+    LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N) := by
   constructor
-  · induction Ns
-    · case nil => grind [multiApp]
-    · case cons N Ns ih => intro h_lc; cases h_lc; grind
+  · induction Ns with
+    | nil  => grind [multiApp]
+    | cons => intro h_lc; cases h_lc; grind
   · induction Ns <;> grind [multiApp, LC.app]
 
 /- just like ordinary beta reduction, the left-hand side
@@ -97,7 +95,7 @@ lemma steps_multiApp_l {M M' : Term Var} {Ns : List (Term Var)}
 omit [DecidableEq Var] [HasFresh Var] in
 @[scoped grind ←]
 lemma step_multiApp_r {M : Term Var} {Ns Ns' : List (Term Var)}
-  (steps : Ns ⭢βᶠ Ns')
+  (steps : Ns ⭢lβᶠ Ns')
   (lc_M : LC M) :
     M.multiApp Ns ⭢βᶠ M.multiApp Ns' := by
   induction steps <;> grind [multiApp, FullBeta.appL, FullBeta.appR]
@@ -106,7 +104,7 @@ lemma step_multiApp_r {M : Term Var} {Ns Ns' : List (Term Var)}
 omit [DecidableEq Var] [HasFresh Var] in
 @[scoped grind ←]
 lemma steps_multiApp_r {M : Term Var} {Ns Ns' : List (Term Var)}
-  (steps : Ns ↠βᶠ Ns')
+  (steps : Ns ↠lβᶠ Ns')
   (lc_M : LC M) :
     M.multiApp Ns ↠βᶠ M.multiApp Ns' := by
   induction steps <;> grind [multiApp, FullBeta.appL, FullBeta.appR]
@@ -123,15 +121,15 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
   (h_red : multiApp (M.abs.app N) Ps ⭢βᶠ Q) :
     (∃ M', M.abs ⭢βᶠ Term.abs M' ∧ Q = multiApp (M'.abs.app N) Ps) ∨
     (∃ N', N ⭢βᶠ N' ∧ Q = multiApp (M.abs.app N') Ps) ∨
-    (∃ Ps', Ps ⭢βᶠ Ps' ∧ Q = multiApp (M.abs.app N) Ps') ∨
+    (∃ Ps', Ps ⭢lβᶠ Ps' ∧ Q = multiApp (M.abs.app N) Ps') ∨
     (Q = multiApp (M ^ N) Ps) := by
   induction Ps generalizing M N Q with
   | nil =>
     rw [multiApp] at h_red
     rw [multiApp]
     cases h_red
-    · case beta abs_lc n_lc => aesop
-    · case appL M N' lc_z h_red => aesop
+    · case beta abs_lc n_lc => grind
+    · case appL M N' lc_z h_red => grind
     · case appR M M' lc_z h_red =>
         left
         cases lc_z
@@ -150,20 +148,16 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
     · case beta abs_lc n_lc => cases Ps <;> contradiction
     · case appL Y M P' lc_z h_red =>
         right; right; left
-        exists (P' :: Ps)
-        simp
-        grind
+        exists (P' :: Ps); grind
     · case appR M Q'' h_red P_lc =>
         rw [←Heq] at h_red
         match (ih h_red) with
-        | .inl ⟨ M', st, Heq' ⟩                => aesop
-        | .inr (.inl ⟨ N', st, Heq' ⟩)         => aesop
+        | .inl ⟨ M', st, Heq' ⟩                => grind
+        | .inr (.inl ⟨ N', st, Heq' ⟩)         => grind
         | .inr (.inr (.inl ⟨ Ps', st, Heq' ⟩)) =>
           right; right; left
-          exists (P :: Ps')
-          simp
-          grind
-        | .inr (.inr (.inr Heq'))              => aesop
+          exists (P :: Ps');grind
+        | .inr (.inr (.inr Heq'))              => grind
 
 /- if a term (λ M) N P_1 ... P_n reduces in multiple steps to Q, then either Q if of the form
 
@@ -183,10 +177,10 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
 -/
 lemma invert_abs_multiApp_mst {Ps} {M N Q : Term Var}
   (h_red : multiApp (M.abs.app N) Ps ↠βᶠ Q) :
-    ∃ M' N' Ns', M.abs ↠βᶠ M'.abs ∧ N ↠βᶠ N' ∧ Ps ↠βᶠ Ns' ∧
+    ∃ M' N' Ns', M.abs ↠βᶠ M'.abs ∧ N ↠βᶠ N' ∧ Ps ↠lβᶠ Ns' ∧
                  (Q = multiApp (M'.abs.app N') Ns' ∨
      (multiApp (M.abs.app N) Ps ↠βᶠ multiApp (M' ^ N') Ns' ∧
-                                      multiApp (M' ^ N') Ns' ↠βᶠ Q)) := by
+                                     multiApp (M' ^ N') Ns' ↠βᶠ Q)) := by
   induction h_red
   · case refl => grind
   · case tail Q' Q'' steps step ih =>

From 44683a1523961075cc25dbd6d22073570b167bdd Mon Sep 17 00:00:00 2001
From: David Wegmann <david.wegmann@fau.de>
Date: Sat, 7 Mar 2026 23:06:08 +0100
Subject: [PATCH 13/22] added section variables to reduce hypothesis clutter

---
 .../LocallyNameless/Untyped/MultiApp.lean     | 39 ++++++++-----------
 1 file changed, 17 insertions(+), 22 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 086c71518..45e7c1f96 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -23,9 +23,11 @@ variable {Var : Type u} [DecidableEq Var] [HasFresh Var]
 namespace LambdaCalculus.LocallyNameless.Untyped.Term
 
 
+
+
 /-
-  multiApp f [x_1, x_2, ..., x_n] applies the arguments x_1, x_2, ..., x_n
-  to f in left-associative order, i.e. as (((f x_1) x_2) ... x_n).
+  multiApp f [x₁, x₂, ..., xₙ] applies the arguments x₁, x₂, ..., xₙ
+  to f in left-associative order, i.e. as (((f x₁) x₂) ... xₙ).
 -/
 @[simp, scoped grind =]
 def multiApp (f : Term Var) (args : List (Term Var)) :=
@@ -48,15 +50,16 @@ inductive list_full_beta : List (Term Var) → List (Term Var) → Prop where
 
 attribute [scoped grind .] list_full_beta.step list_full_beta.cons
 
+variable {M M' : Term Var} {Ns Ns' : List (Term Var)}
+
 /- just like ordinary beta reduction, the right-hand side
    of a multi-application step is locally closed -/
-lemma multiApp_step_lc_r {Ns Ns' : List (Term Var)} (step : Ns ⭢lβᶠ Ns') :
+lemma multiApp_step_lc_r (step : Ns ⭢lβᶠ Ns') :
     (∀ N ∈ Ns', LC N) := by
   induction step <;> grind [FullBeta.step_lc_r]
 
 /- just like ordinary beta reduction, multiple steps of a argument list preserves local closure -/
-lemma multiApp_steps_lc {Ns Ns' : List (Term Var)}
-  (step : Ns ↠lβᶠ Ns') (H : ∀ N ∈ Ns, LC N) :
+lemma multiApp_steps_lc (step : Ns ↠lβᶠ Ns') (H : ∀ N ∈ Ns, LC N) :
     (∀ N ∈ Ns', LC N) := by
   induction step <;> grind [FullBeta.step_lc_r, multiApp_step_lc_r]
 
@@ -64,7 +67,7 @@ lemma multiApp_steps_lc {Ns Ns' : List (Term Var)}
    and only if the leftmost term and all arguments applied to it are locally closed -/
 omit [DecidableEq Var] [HasFresh Var] in
 @[scoped grind ←]
-lemma multiApp_lc {M : Term Var} {Ns : List (Term Var)} :
+lemma multiApp_lc :
     LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N) := by
   constructor
   · induction Ns with
@@ -76,36 +79,28 @@ lemma multiApp_lc {M : Term Var} {Ns : List (Term Var)} :
    of a multi-application step is locally closed -/
 omit [DecidableEq Var] [HasFresh Var] in
 @[scoped grind ←]
-lemma step_multiApp_l {M M' : Term Var} {Ns : List (Term Var)}
-  (steps : M ⭢βᶠ M')
-  (lc_Ns : ∀ N ∈ Ns, LC N) :
+lemma step_multiApp_l (steps : M ⭢βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) :
     M.multiApp Ns ⭢βᶠ M'.multiApp Ns := by
   induction Ns <;> grind [multiApp, FullBeta.appR]
 
 /- congruence lemma for multi reduction of the left most term of a multi-application -/
 omit [DecidableEq Var] [HasFresh Var] in
 @[scoped grind ←]
-lemma steps_multiApp_l {M M' : Term Var} {Ns : List (Term Var)}
-  (steps : M ↠βᶠ M')
-  (lc_Ns : ∀ N ∈ Ns, LC N) :
+lemma steps_multiApp_l (steps : M ↠βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) :
     M.multiApp Ns ↠βᶠ M'.multiApp Ns := by
   induction steps <;> grind
 
 /- congruence lemma for single reduction of one of the arguments of a multi-application -/
 omit [DecidableEq Var] [HasFresh Var] in
 @[scoped grind ←]
-lemma step_multiApp_r {M : Term Var} {Ns Ns' : List (Term Var)}
-  (steps : Ns ⭢lβᶠ Ns')
-  (lc_M : LC M) :
+lemma step_multiApp_r (steps : Ns ⭢lβᶠ Ns') (lc_M : LC M) :
     M.multiApp Ns ⭢βᶠ M.multiApp Ns' := by
   induction steps <;> grind [multiApp, FullBeta.appL, FullBeta.appR]
 
 /- congruence lemma for multiple reduction of one of the arguments of a multi-application -/
 omit [DecidableEq Var] [HasFresh Var] in
 @[scoped grind ←]
-lemma steps_multiApp_r {M : Term Var} {Ns Ns' : List (Term Var)}
-  (steps : Ns ↠lβᶠ Ns')
-  (lc_M : LC M) :
+lemma steps_multiApp_r (steps : Ns ↠lβᶠ Ns') (lc_M : LC M) :
     M.multiApp Ns ↠βᶠ M.multiApp Ns' := by
   induction steps <;> grind [multiApp, FullBeta.appL, FullBeta.appR]
 
@@ -159,19 +154,19 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
           exists (P :: Ps');grind
         | .inr (.inr (.inr Heq'))              => grind
 
-/- if a term (λ M) N P_1 ... P_n reduces in multiple steps to Q, then either Q if of the form
+/- if a term (λ M) N P₁ ... Pₙ reduces in multiple steps to Q, then either Q if of the form
 
-    Q = (λ M') N' P'_1 ... P'_n
+    Q = (λ M') N' P'₁ ... P'ₙ
 
    or
 
     we first reach an intermediate term of this shape,
 
-    (λ M) N P_1 ... P_n ↠βᶠ (λ M') N' P'_1 ... P'_n
+    (λ M) N P₁ ... Pₙ ↠βᶠ (λ M') N' P'₁ ... P'ₙ
 
     then perform a beta reduction and reduce further to Q
 
-    (λ M') N' P'_1 ... P'_n ↠βᶠ M' ^ N' P'_1 ... P'_n ↠βᶠ Q
+    (λ M') N' P'₁ ... P'ₙ ↠βᶠ M' ^ N' P'_₁ ... P'_ₙ ↠βᶠ Q
 
    where M ↠βᶠ M' and N ↠βᶠ N' and P_i ↠βᶠ P_i' for all i,
 -/

From 06885f96c734d6c361b4437c522b6e333ff3ac06 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 8 Mar 2026 05:35:46 -0400
Subject: [PATCH 14/22] some style work

---
 .../LocallyNameless/Untyped/MultiApp.lean     | 72 ++++++++-----------
 1 file changed, 29 insertions(+), 43 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 45e7c1f96..7a76eb1af 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -18,22 +18,18 @@ namespace Cslib
 
 universe u
 
-variable {Var : Type u} [DecidableEq Var] [HasFresh Var]
+variable {Var : Type u}
 
 namespace LambdaCalculus.LocallyNameless.Untyped.Term
 
-
-
-
 /-
   multiApp f [x₁, x₂, ..., xₙ] applies the arguments x₁, x₂, ..., xₙ
   to f in left-associative order, i.e. as (((f x₁) x₂) ... xₙ).
 -/
 @[simp, scoped grind =]
-def multiApp (f : Term Var) (args : List (Term Var)) :=
-  match args with
-  | []      => f
-  | a :: as => Term.app (multiApp f as) a
+def multiApp (f : Term Var) : List (Term Var) → Term Var
+| []      => f
+| a :: as => Term.app (multiApp f as) a
 
 /-
   A list of arguments performs a single reduction step
@@ -43,68 +39,58 @@ def multiApp (f : Term Var) (args : List (Term Var)) :=
   if one of the arguments performs a single step xᵢ ⭢βᶠ xᵢ'
   and the rest of the arguments are locally closed.
 -/
-@[reduction_sys "lβᶠ"]
-inductive list_full_beta : List (Term Var) → List (Term Var) → Prop where
-| step : N ⭢βᶠ N' → (∀ N ∈ Ns, LC N) → list_full_beta (N :: Ns) (N' :: Ns)
-| cons : LC N → list_full_beta Ns Ns' → list_full_beta (N :: Ns) (N :: Ns')
-
-attribute [scoped grind .] list_full_beta.step list_full_beta.cons
+@[scoped grind, reduction_sys "lβᶠ"]
+inductive ListFullBeta : List (Term Var) → List (Term Var) → Prop where
+| step : N ⭢βᶠ N' → (∀ N ∈ Ns, LC N) → ListFullBeta (N :: Ns) (N' :: Ns)
+| cons : LC N → ListFullBeta Ns Ns' → ListFullBeta (N :: Ns) (N :: Ns')
 
 variable {M M' : Term Var} {Ns Ns' : List (Term Var)}
 
-/- just like ordinary beta reduction, the right-hand side
-   of a multi-application step is locally closed -/
-lemma multiApp_step_lc_r (step : Ns ⭢lβᶠ Ns') :
-    (∀ N ∈ Ns', LC N) := by
-  induction step <;> grind [FullBeta.step_lc_r]
-
-/- just like ordinary beta reduction, multiple steps of a argument list preserves local closure -/
-lemma multiApp_steps_lc (step : Ns ↠lβᶠ Ns') (H : ∀ N ∈ Ns, LC N) :
-    (∀ N ∈ Ns', LC N) := by
-  induction step <;> grind [FullBeta.step_lc_r, multiApp_step_lc_r]
-
-/- a term resulting from a multi-application is locally closed if
+/- A term resulting from a multi-application is locally closed if
    and only if the leftmost term and all arguments applied to it are locally closed -/
-omit [DecidableEq Var] [HasFresh Var] in
 @[scoped grind ←]
-lemma multiApp_lc :
-    LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N) := by
+lemma multiApp_lc : LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N) := by
   constructor
   · induction Ns with
     | nil  => grind [multiApp]
     | cons => intro h_lc; cases h_lc; grind
   · induction Ns <;> grind [multiApp, LC.app]
 
-/- just like ordinary beta reduction, the left-hand side
+/- Just like ordinary beta reduction, the left-hand side
    of a multi-application step is locally closed -/
-omit [DecidableEq Var] [HasFresh Var] in
 @[scoped grind ←]
 lemma step_multiApp_l (steps : M ⭢βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) :
     M.multiApp Ns ⭢βᶠ M'.multiApp Ns := by
   induction Ns <;> grind [multiApp, FullBeta.appR]
 
-/- congruence lemma for multi reduction of the left most term of a multi-application -/
-omit [DecidableEq Var] [HasFresh Var] in
+/- Congruence lemma for multi reduction of the left most term of a multi-application -/
 @[scoped grind ←]
 lemma steps_multiApp_l (steps : M ↠βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) :
     M.multiApp Ns ↠βᶠ M'.multiApp Ns := by
   induction steps <;> grind
 
-/- congruence lemma for single reduction of one of the arguments of a multi-application -/
-omit [DecidableEq Var] [HasFresh Var] in
+/- Congruence lemma for single reduction of one of the arguments of a multi-application -/
 @[scoped grind ←]
-lemma step_multiApp_r (steps : Ns ⭢lβᶠ Ns') (lc_M : LC M) :
-    M.multiApp Ns ⭢βᶠ M.multiApp Ns' := by
+lemma step_multiApp_r (steps : Ns ⭢lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns ⭢βᶠ M.multiApp Ns' := by
   induction steps <;> grind [multiApp, FullBeta.appL, FullBeta.appR]
 
-/- congruence lemma for multiple reduction of one of the arguments of a multi-application -/
-omit [DecidableEq Var] [HasFresh Var] in
+/- Congruence lemma for multiple reduction of one of the arguments of a multi-application -/
 @[scoped grind ←]
-lemma steps_multiApp_r (steps : Ns ↠lβᶠ Ns') (lc_M : LC M) :
-    M.multiApp Ns ↠βᶠ M.multiApp Ns' := by
+lemma steps_multiApp_r (steps : Ns ↠lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns ↠βᶠ M.multiApp Ns' := by
   induction steps <;> grind [multiApp, FullBeta.appL, FullBeta.appR]
 
-/- if a term (λ M) N P_1 ... P_n reduces in a single step to Q, then
+variable [DecidableEq Var] [HasFresh Var]
+
+/- Just like ordinary beta reduction, the right-hand side
+   of a multi-application step is locally closed -/
+lemma multiApp_step_lc_r (step : Ns ⭢lβᶠ Ns') : ∀ N ∈ Ns', LC N := by
+  induction step <;> grind [FullBeta.step_lc_r]
+
+/- Just like ordinary beta reduction, multiple steps of a argument list preserves local closure -/
+lemma multiApp_steps_lc (step : Ns ↠lβᶠ Ns') (H : ∀ N ∈ Ns, LC N) : ∀ N ∈ Ns', LC N := by
+  induction step <;> grind [FullBeta.step_lc_r, multiApp_step_lc_r]
+
+/- If a term (λ M) N P_1 ... P_n reduces in a single step to Q, then
    Q must be one of the following forms:
 
     Q = (λ M') N P₁ ... Pₙ where M ⭢βᶠ M' or
@@ -154,7 +140,7 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
           exists (P :: Ps');grind
         | .inr (.inr (.inr Heq'))              => grind
 
-/- if a term (λ M) N P₁ ... Pₙ reduces in multiple steps to Q, then either Q if of the form
+/- If a term (λ M) N P₁ ... Pₙ reduces in multiple steps to Q, then either Q if of the form
 
     Q = (λ M') N' P'₁ ... P'ₙ
 

From a92f85ef50fc87cab97f6f91a6ec084824f0d62d Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 8 Mar 2026 05:37:56 -0400
Subject: [PATCH 15/22] rm extra params to grind

---
 .../LocallyNameless/Untyped/MultiApp.lean              | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 7a76eb1af..171957d41 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -52,16 +52,16 @@ variable {M M' : Term Var} {Ns Ns' : List (Term Var)}
 lemma multiApp_lc : LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N) := by
   constructor
   · induction Ns with
-    | nil  => grind [multiApp]
+    | nil  => grind
     | cons => intro h_lc; cases h_lc; grind
-  · induction Ns <;> grind [multiApp, LC.app]
+  · induction Ns <;> grind
 
 /- Just like ordinary beta reduction, the left-hand side
    of a multi-application step is locally closed -/
 @[scoped grind ←]
 lemma step_multiApp_l (steps : M ⭢βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) :
     M.multiApp Ns ⭢βᶠ M'.multiApp Ns := by
-  induction Ns <;> grind [multiApp, FullBeta.appR]
+  induction Ns <;> grind [FullBeta.appR]
 
 /- Congruence lemma for multi reduction of the left most term of a multi-application -/
 @[scoped grind ←]
@@ -72,12 +72,12 @@ lemma steps_multiApp_l (steps : M ↠βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) :
 /- Congruence lemma for single reduction of one of the arguments of a multi-application -/
 @[scoped grind ←]
 lemma step_multiApp_r (steps : Ns ⭢lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns ⭢βᶠ M.multiApp Ns' := by
-  induction steps <;> grind [multiApp, FullBeta.appL, FullBeta.appR]
+  induction steps <;> grind [FullBeta.appL, FullBeta.appR]
 
 /- Congruence lemma for multiple reduction of one of the arguments of a multi-application -/
 @[scoped grind ←]
 lemma steps_multiApp_r (steps : Ns ↠lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns ↠βᶠ M.multiApp Ns' := by
-  induction steps <;> grind [multiApp, FullBeta.appL, FullBeta.appR]
+  induction steps <;> grind [FullBeta.appL, FullBeta.appR]
 
 variable [DecidableEq Var] [HasFresh Var]
 

From a4ee71b08458ff42bb2fac022e30bfb724654340 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 8 Mar 2026 05:53:29 -0400
Subject: [PATCH 16/22] golf invert_abs_multiApp_mst

---
 .../LocallyNameless/Untyped/MultiApp.lean     | 22 +++++++------------
 1 file changed, 8 insertions(+), 14 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 171957d41..374459200 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -162,20 +162,14 @@ lemma invert_abs_multiApp_mst {Ps} {M N Q : Term Var}
                  (Q = multiApp (M'.abs.app N') Ns' ∨
      (multiApp (M.abs.app N) Ps ↠βᶠ multiApp (M' ^ N') Ns' ∧
                                      multiApp (M' ^ N') Ns' ↠βᶠ Q)) := by
-  induction h_red
-  · case refl => grind
-  · case tail Q' Q'' steps step ih =>
-    match ih with
-    | ⟨ M', N', Ps', st_M, st_N, st_Ps, Cases ⟩ =>
-      match Cases with
-      | .inl Heq =>
-        rw [Heq] at step
-        match (invert_abs_multiApp_st step) with
-        | .inl ⟨ M'', st, HeqM'' ⟩             => grind
-        | .inr (.inl ⟨ N', st, Heq' ⟩)         => grind
-        | .inr (.inr (.inl ⟨ Ps', st, Heq' ⟩)) => grind
-        | .inr (.inr (.inr Heq'))              => grind
-      | .inr ⟨ steps1, steps2 ⟩ => grind [Relation.ReflTransGen.single]
+  induction h_red with
+  | refl => grind
+  | tail _ step ih =>
+    obtain ⟨_, _, _, _, _, _, h⟩ := ih
+    rcases h with heq | _
+    · subst heq
+      grind [invert_abs_multiApp_st step]
+    · grind [Relation.ReflTransGen.single]
 
 end LambdaCalculus.LocallyNameless.Untyped.Term
 

From a03d1279971df958b495e55edb2631c5f8a01d53 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 8 Mar 2026 06:39:32 -0400
Subject: [PATCH 17/22] golf invert_abs_multiApp_st

---
 .../LocallyNameless/Untyped/MultiApp.lean     | 67 ++++++-------------
 1 file changed, 19 insertions(+), 48 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 374459200..3092536e4 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -50,11 +50,7 @@ variable {M M' : Term Var} {Ns Ns' : List (Term Var)}
    and only if the leftmost term and all arguments applied to it are locally closed -/
 @[scoped grind ←]
 lemma multiApp_lc : LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N) := by
-  constructor
-  · induction Ns with
-    | nil  => grind
-    | cons => intro h_lc; cases h_lc; grind
-  · induction Ns <;> grind
+  induction Ns with grind [cases LC]
 
 /- Just like ordinary beta reduction, the left-hand side
    of a multi-application step is locally closed -/
@@ -79,17 +75,6 @@ lemma step_multiApp_r (steps : Ns ⭢lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns 
 lemma steps_multiApp_r (steps : Ns ↠lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns ↠βᶠ M.multiApp Ns' := by
   induction steps <;> grind [FullBeta.appL, FullBeta.appR]
 
-variable [DecidableEq Var] [HasFresh Var]
-
-/- Just like ordinary beta reduction, the right-hand side
-   of a multi-application step is locally closed -/
-lemma multiApp_step_lc_r (step : Ns ⭢lβᶠ Ns') : ∀ N ∈ Ns', LC N := by
-  induction step <;> grind [FullBeta.step_lc_r]
-
-/- Just like ordinary beta reduction, multiple steps of a argument list preserves local closure -/
-lemma multiApp_steps_lc (step : Ns ↠lβᶠ Ns') (H : ∀ N ∈ Ns, LC N) : ∀ N ∈ Ns', LC N := by
-  induction step <;> grind [FullBeta.step_lc_r, multiApp_step_lc_r]
-
 /- If a term (λ M) N P_1 ... P_n reduces in a single step to Q, then
    Q must be one of the following forms:
 
@@ -105,40 +90,15 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
     (∃ Ps', Ps ⭢lβᶠ Ps' ∧ Q = multiApp (M.abs.app N) Ps') ∨
     (Q = multiApp (M ^ N) Ps) := by
   induction Ps generalizing M N Q with
-  | nil =>
-    rw [multiApp] at h_red
-    rw [multiApp]
-    cases h_red
-    · case beta abs_lc n_lc => grind
-    · case appL M N' lc_z h_red => grind
-    · case appR M M' lc_z h_red =>
-        left
-        cases lc_z
-        · case abs M' xs h_lc =>
-            exists M'
-            constructor
-            · apply FullBeta.step_abs_cong
-              assumption
-            · rfl
+  | nil => grind [cases FullBeta]
   | cons P Ps ih =>
-    have h_lc := (FullBeta.step_lc_l h_red)
-    rw [multiApp] at h_red
     generalize Heq : (M.abs.app N).multiApp Ps = Q'
-    rw [Heq] at h_red
-    cases h_red
-    · case beta abs_lc n_lc => cases Ps <;> contradiction
-    · case appL Y M P' lc_z h_red =>
-        right; right; left
-        exists (P' :: Ps); grind
-    · case appR M Q'' h_red P_lc =>
-        rw [←Heq] at h_red
-        match (ih h_red) with
-        | .inl ⟨ M', st, Heq' ⟩                => grind
-        | .inr (.inl ⟨ N', st, Heq' ⟩)         => grind
-        | .inr (.inr (.inl ⟨ Ps', st, Heq' ⟩)) =>
-          right; right; left
-          exists (P :: Ps');grind
-        | .inr (.inr (.inr Heq'))              => grind
+    have : ∀ P', Q'.app P' = (M.abs.app N).multiApp (P' :: Ps) := by grind
+    rw [multiApp, Heq] at h_red
+    cases h_red with
+    | beta => cases Ps <;> contradiction
+    | appR => grind [→ ListFullBeta.cons]
+    | appL => grind
 
 /- If a term (λ M) N P₁ ... Pₙ reduces in multiple steps to Q, then either Q if of the form
 
@@ -171,6 +131,17 @@ lemma invert_abs_multiApp_mst {Ps} {M N Q : Term Var}
       grind [invert_abs_multiApp_st step]
     · grind [Relation.ReflTransGen.single]
 
+variable [DecidableEq Var] [HasFresh Var]
+
+/- Just like ordinary beta reduction, the right-hand side
+   of a multi-application step is locally closed -/
+lemma multiApp_step_lc_r (step : Ns ⭢lβᶠ Ns') : ∀ N ∈ Ns', LC N := by
+  induction step <;> grind [FullBeta.step_lc_r]
+
+/- Just like ordinary beta reduction, multiple steps of a argument list preserves local closure -/
+lemma multiApp_steps_lc (step : Ns ↠lβᶠ Ns') (H : ∀ N ∈ Ns, LC N) : ∀ N ∈ Ns', LC N := by
+  induction step <;> grind [FullBeta.step_lc_r, multiApp_step_lc_r]
+
 end LambdaCalculus.LocallyNameless.Untyped.Term
 
 end Cslib

From eb1e9eb1a0b74ea6bfbbe509e184cf277a4779a4 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 8 Mar 2026 07:20:54 -0400
Subject: [PATCH 18/22] grind_lint

---
 .../LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean        | 2 --
 CslibTests/GrindLint.lean                                       | 2 ++
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 3092536e4..4d6ef75da 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -60,7 +60,6 @@ lemma step_multiApp_l (steps : M ⭢βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) :
   induction Ns <;> grind [FullBeta.appR]
 
 /- Congruence lemma for multi reduction of the left most term of a multi-application -/
-@[scoped grind ←]
 lemma steps_multiApp_l (steps : M ↠βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) :
     M.multiApp Ns ↠βᶠ M'.multiApp Ns := by
   induction steps <;> grind
@@ -71,7 +70,6 @@ lemma step_multiApp_r (steps : Ns ⭢lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns 
   induction steps <;> grind [FullBeta.appL, FullBeta.appR]
 
 /- Congruence lemma for multiple reduction of one of the arguments of a multi-application -/
-@[scoped grind ←]
 lemma steps_multiApp_r (steps : Ns ↠lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns ↠βᶠ M.multiApp Ns' := by
   induction steps <;> grind [FullBeta.appL, FullBeta.appR]
 
diff --git a/CslibTests/GrindLint.lean b/CslibTests/GrindLint.lean
index 67673a40b..8c456a6c2 100644
--- a/CslibTests/GrindLint.lean
+++ b/CslibTests/GrindLint.lean
@@ -72,6 +72,8 @@ open_scoped_all Cslib
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.redex_app_l_cong
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBeta.redex_app_r_cong
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.subst_intro
+#grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.ListFullBeta.cons
+#grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.ListFullBeta.step
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.sub
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.ty
 #grind_lint skip Cslib.Logic.HML.bisimulation_satisfies

From 6de1a4d7927f36ca8ba34d01047280e81181928f Mon Sep 17 00:00:00 2001
From: David Wegmann <david.wegmann@fau.de>
Date: Sun, 8 Mar 2026 16:14:03 +0100
Subject: [PATCH 19/22] added docstring

---
 .../LocallyNameless/Untyped/MultiApp.lean            | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 4d6ef75da..e24d094df 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -24,8 +24,7 @@ namespace LambdaCalculus.LocallyNameless.Untyped.Term
 
 /-
   multiApp f [x₁, x₂, ..., xₙ] applies the arguments x₁, x₂, ..., xₙ
-  to f in left-associative order, i.e. as (((f x₁) x₂) ... xₙ).
--/
+  to f in left-associative order, i.e. as (((f x₁) x₂) ... xₙ). -/
 @[simp, scoped grind =]
 def multiApp (f : Term Var) : List (Term Var) → Term Var
 | []      => f
@@ -37,8 +36,7 @@ def multiApp (f : Term Var) : List (Term Var) → Term Var
   [x₁, ..., xᵢ ..., xₙ] ⭢βᶠ [x₁, ..., xᵢ', ..., xₙ]
 
   if one of the arguments performs a single step xᵢ ⭢βᶠ xᵢ'
-  and the rest of the arguments are locally closed.
--/
+  and the rest of the arguments are locally closed. -/
 @[scoped grind, reduction_sys "lβᶠ"]
 inductive ListFullBeta : List (Term Var) → List (Term Var) → Prop where
 | step : N ⭢βᶠ N' → (∀ N ∈ Ns, LC N) → ListFullBeta (N :: Ns) (N' :: Ns)
@@ -79,8 +77,7 @@ lemma steps_multiApp_r (steps : Ns ↠lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns
     Q = (λ M') N P₁ ... Pₙ where M ⭢βᶠ M' or
     Q = (λ M) N' P₁ ... Pₙ where N ⭢βᶠ N' or
     Q = (λ M) N P₁' ... Pₙ' where P_i ⭢βᶠ P_i' for some i or
-    Q = (M ^ N) P₁ ... Pₙ
--/
+    Q = (M ^ N) P₁ ... Pₙ -/
 lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
   (h_red : multiApp (M.abs.app N) Ps ⭢βᶠ Q) :
     (∃ M', M.abs ⭢βᶠ Term.abs M' ∧ Q = multiApp (M'.abs.app N) Ps) ∨
@@ -112,8 +109,7 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
 
     (λ M') N' P'₁ ... P'ₙ ↠βᶠ M' ^ N' P'_₁ ... P'_ₙ ↠βᶠ Q
 
-   where M ↠βᶠ M' and N ↠βᶠ N' and P_i ↠βᶠ P_i' for all i,
--/
+   where M ↠βᶠ M' and N ↠βᶠ N' and P_i ↠βᶠ P_i' for all i, -/
 lemma invert_abs_multiApp_mst {Ps} {M N Q : Term Var}
   (h_red : multiApp (M.abs.app N) Ps ↠βᶠ Q) :
     ∃ M' N' Ns', M.abs ↠βᶠ M'.abs ∧ N ↠βᶠ N' ∧ Ps ↠lβᶠ Ns' ∧

From 9a5ccef24666f4e93af4cac1ddabbb67dc24404a Mon Sep 17 00:00:00 2001
From: David Wegmann <david.wegmann@fau.de>
Date: Sun, 8 Mar 2026 16:27:44 +0100
Subject: [PATCH 20/22] added docstrings to constructors of ListFullBeta

---
 .../LocallyNameless/Untyped/MultiApp.lean        | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index e24d094df..a846aa5e7 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -22,24 +22,24 @@ variable {Var : Type u}
 
 namespace LambdaCalculus.LocallyNameless.Untyped.Term
 
-/-
-  multiApp f [x₁, x₂, ..., xₙ] applies the arguments x₁, x₂, ..., xₙ
-  to f in left-associative order, i.e. as (((f x₁) x₂) ... xₙ). -/
+/- multiApp f [x₁, x₂, ..., xₙ] applies the arguments x₁, x₂, ..., xₙ
+   to f in left-associative order, i.e. as (((f x₁) x₂) ... xₙ). -/
 @[simp, scoped grind =]
 def multiApp (f : Term Var) : List (Term Var) → Term Var
 | []      => f
 | a :: as => Term.app (multiApp f as) a
 
-/-
-  A list of arguments performs a single reduction step
+/- A list of arguments performs a single reduction step
 
-  [x₁, ..., xᵢ ..., xₙ] ⭢βᶠ [x₁, ..., xᵢ', ..., xₙ]
+   [x₁, ..., xᵢ ..., xₙ] ⭢βᶠ [x₁, ..., xᵢ', ..., xₙ]
 
-  if one of the arguments performs a single step xᵢ ⭢βᶠ xᵢ'
-  and the rest of the arguments are locally closed. -/
+   if one of the arguments performs a single step xᵢ ⭢βᶠ xᵢ'
+   and the rest of the arguments are locally closed. -/
 @[scoped grind, reduction_sys "lβᶠ"]
 inductive ListFullBeta : List (Term Var) → List (Term Var) → Prop where
+/- head of the list performs a single reduction step, the rest are locally closed -/
 | step : N ⭢βᶠ N' → (∀ N ∈ Ns, LC N) → ListFullBeta (N :: Ns) (N' :: Ns)
+/- given a list that already contains a step, we can add locally closed terms to the front -/
 | cons : LC N → ListFullBeta Ns Ns' → ListFullBeta (N :: Ns) (N :: Ns')
 
 variable {M M' : Term Var} {Ns Ns' : List (Term Var)}

From f2b52e923adf58cc54b98bba80b161ca8277a4c2 Mon Sep 17 00:00:00 2001
From: David Wegmann <david.wegmann@fau.de>
Date: Sun, 8 Mar 2026 22:22:44 +0100
Subject: [PATCH 21/22] changed /- to /-- for docstrings to work

---
 .../LocallyNameless/Untyped/MultiApp.lean     | 52 +++++++++----------
 1 file changed, 26 insertions(+), 26 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index a846aa5e7..e135287e5 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -22,57 +22,57 @@ variable {Var : Type u}
 
 namespace LambdaCalculus.LocallyNameless.Untyped.Term
 
-/- multiApp f [x₁, x₂, ..., xₙ] applies the arguments x₁, x₂, ..., xₙ
-   to f in left-associative order, i.e. as (((f x₁) x₂) ... xₙ). -/
+/-- multiApp f [x₁, x₂, ..., xₙ] applies the arguments x₁, x₂, ..., xₙ
+    to f in left-associative order, i.e. as (((f x₁) x₂) ... xₙ). -/
 @[simp, scoped grind =]
 def multiApp (f : Term Var) : List (Term Var) → Term Var
 | []      => f
 | a :: as => Term.app (multiApp f as) a
 
-/- A list of arguments performs a single reduction step
+/-- A list of arguments performs a single reduction step
 
-   [x₁, ..., xᵢ ..., xₙ] ⭢βᶠ [x₁, ..., xᵢ', ..., xₙ]
+    [x₁, ..., xᵢ ..., xₙ] ⭢βᶠ [x₁, ..., xᵢ', ..., xₙ]
 
-   if one of the arguments performs a single step xᵢ ⭢βᶠ xᵢ'
-   and the rest of the arguments are locally closed. -/
+    if one of the arguments performs a single step xᵢ ⭢βᶠ xᵢ'
+    and the rest of the arguments are locally closed. -/
 @[scoped grind, reduction_sys "lβᶠ"]
 inductive ListFullBeta : List (Term Var) → List (Term Var) → Prop where
-/- head of the list performs a single reduction step, the rest are locally closed -/
+/-- head of the list performs a single reduction step, the rest are locally closed -/
 | step : N ⭢βᶠ N' → (∀ N ∈ Ns, LC N) → ListFullBeta (N :: Ns) (N' :: Ns)
-/- given a list that already contains a step, we can add locally closed terms to the front -/
+/-- given a list that already contains a step, we can add locally closed terms to the front -/
 | cons : LC N → ListFullBeta Ns Ns' → ListFullBeta (N :: Ns) (N :: Ns')
 
 variable {M M' : Term Var} {Ns Ns' : List (Term Var)}
 
-/- A term resulting from a multi-application is locally closed if
-   and only if the leftmost term and all arguments applied to it are locally closed -/
+/-- A term resulting from a multi-application is locally closed if
+    and only if the leftmost term and all arguments applied to it are locally closed -/
 @[scoped grind ←]
 lemma multiApp_lc : LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N) := by
   induction Ns with grind [cases LC]
 
-/- Just like ordinary beta reduction, the left-hand side
-   of a multi-application step is locally closed -/
+/-- Just like ordinary beta reduction, the left-hand side
+    of a multi-application step is locally closed -/
 @[scoped grind ←]
 lemma step_multiApp_l (steps : M ⭢βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) :
     M.multiApp Ns ⭢βᶠ M'.multiApp Ns := by
   induction Ns <;> grind [FullBeta.appR]
 
-/- Congruence lemma for multi reduction of the left most term of a multi-application -/
+/-- Congruence lemma for multi reduction of the left most term of a multi-application -/
 lemma steps_multiApp_l (steps : M ↠βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) :
     M.multiApp Ns ↠βᶠ M'.multiApp Ns := by
   induction steps <;> grind
 
-/- Congruence lemma for single reduction of one of the arguments of a multi-application -/
+/-- Congruence lemma for single reduction of one of the arguments of a multi-application -/
 @[scoped grind ←]
 lemma step_multiApp_r (steps : Ns ⭢lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns ⭢βᶠ M.multiApp Ns' := by
   induction steps <;> grind [FullBeta.appL, FullBeta.appR]
 
-/- Congruence lemma for multiple reduction of one of the arguments of a multi-application -/
+/-- Congruence lemma for multiple reduction of one of the arguments of a multi-application -/
 lemma steps_multiApp_r (steps : Ns ↠lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns ↠βᶠ M.multiApp Ns' := by
   induction steps <;> grind [FullBeta.appL, FullBeta.appR]
 
-/- If a term (λ M) N P_1 ... P_n reduces in a single step to Q, then
-   Q must be one of the following forms:
+/-- If a term (λ M) N P_1 ... P_n reduces in a single step to Q, then
+    Q must be one of the following forms:
 
     Q = (λ M') N P₁ ... Pₙ where M ⭢βᶠ M' or
     Q = (λ M) N' P₁ ... Pₙ where N ⭢βᶠ N' or
@@ -95,19 +95,19 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
     | appR => grind [→ ListFullBeta.cons]
     | appL => grind
 
-/- If a term (λ M) N P₁ ... Pₙ reduces in multiple steps to Q, then either Q if of the form
+/-- If a term (λ M) N P₁ ... Pₙ reduces in multiple steps to Q, then either Q if of the form
 
-    Q = (λ M') N' P'₁ ... P'ₙ
+      Q = (λ M') N' P'₁ ... P'ₙ
 
-   or
+      or
 
     we first reach an intermediate term of this shape,
 
-    (λ M) N P₁ ... Pₙ ↠βᶠ (λ M') N' P'₁ ... P'ₙ
+      (λ M) N P₁ ... Pₙ ↠βᶠ (λ M') N' P'₁ ... P'ₙ
 
-    then perform a beta reduction and reduce further to Q
+      then perform a beta reduction and reduce further to Q
 
-    (λ M') N' P'₁ ... P'ₙ ↠βᶠ M' ^ N' P'_₁ ... P'_ₙ ↠βᶠ Q
+      (λ M') N' P'₁ ... P'ₙ ↠βᶠ M' ^ N' P'_₁ ... P'_ₙ ↠βᶠ Q
 
    where M ↠βᶠ M' and N ↠βᶠ N' and P_i ↠βᶠ P_i' for all i, -/
 lemma invert_abs_multiApp_mst {Ps} {M N Q : Term Var}
@@ -127,12 +127,12 @@ lemma invert_abs_multiApp_mst {Ps} {M N Q : Term Var}
 
 variable [DecidableEq Var] [HasFresh Var]
 
-/- Just like ordinary beta reduction, the right-hand side
-   of a multi-application step is locally closed -/
+/-- Just like ordinary beta reduction, the right-hand side
+    of a multi-application step is locally closed -/
 lemma multiApp_step_lc_r (step : Ns ⭢lβᶠ Ns') : ∀ N ∈ Ns', LC N := by
   induction step <;> grind [FullBeta.step_lc_r]
 
-/- Just like ordinary beta reduction, multiple steps of a argument list preserves local closure -/
+/-- Just like ordinary beta reduction, multiple steps of a argument list preserves local closure -/
 lemma multiApp_steps_lc (step : Ns ↠lβᶠ Ns') (H : ∀ N ∈ Ns, LC N) : ∀ N ∈ Ns', LC N := by
   induction step <;> grind [FullBeta.step_lc_r, multiApp_step_lc_r]
 

From 1d63423af07201c9b3a5b3c2c69c8d26640bf85b Mon Sep 17 00:00:00 2001
From: David Wegmann <david.wegmann@fau.de>
Date: Sun, 8 Mar 2026 22:25:48 +0100
Subject: [PATCH 22/22] removed comma in docstring

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index e135287e5..e34a46dfb 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -109,7 +109,7 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
 
       (λ M') N' P'₁ ... P'ₙ ↠βᶠ M' ^ N' P'_₁ ... P'_ₙ ↠βᶠ Q
 
-   where M ↠βᶠ M' and N ↠βᶠ N' and P_i ↠βᶠ P_i' for all i, -/
+   where M ↠βᶠ M' and N ↠βᶠ N' and P_i ↠βᶠ P_i' for all i -/
 lemma invert_abs_multiApp_mst {Ps} {M N Q : Term Var}
   (h_red : multiApp (M.abs.app N) Ps ↠βᶠ Q) :
     ∃ M' N' Ns', M.abs ↠βᶠ M'.abs ∧ N ↠βᶠ N' ∧ Ps ↠lβᶠ Ns' ∧