From e3103207d2145446114a73bc0e71493758bf0e06 Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Sat, 11 Jul 2026 08:01:56 +0800
Subject: [PATCH 01/10] refactor(LocallyNameless): change multiApp to
 right-recursive + add tail lemma; update proofs

- Redefine `multiApp` as right-recursive (`multiApp (app f a) as`) instead of left.
- Switch several inductions to `List.reverseRecOn` for better compatibility with the new recursion.
- Add `listFullBeta_cons_r`/`listFullBeta_cons_l`/`multiApp_tail`  helpers.
- Update `invert_abs_multiApp_st`, `sn_abs_app_multiApp`, `multiApp_lc`, reduction congruences, etc.
- Minor tactic adjustment in `Stlc/StrongNorm`.

Fixes #706
---
 .../LocallyNameless/Stlc/StrongNorm.lean      |  3 +-
 .../LocallyNameless/Untyped/MultiApp.lean     | 51 ++++++++++++++-----
 .../LocallyNameless/Untyped/StrongNorm.lean   | 19 ++++---
 3 files changed, 53 insertions(+), 20 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
index 783ec90ff..323fa056f 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
@@ -71,7 +71,8 @@ lemma semanticMap_saturated (τ : Ty Base) : @Saturated Var (semanticMap τ) :=
     · grind [sn_app_left (Var := Var) (N := fvar <| fresh {})]
     · grind
     · intro M N P _ _ _ s _
-      grind [ih₂.multiApp M N (s :: P)]
+      have := ih₂.multiApp M N (P ++ [s])
+      grind [multiApp_tail]
 
 /-- The `entailsContext` predicate ensures that each variable in the context
     is mapped to a term in the corresponding semantic map. -/
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index d7016d7dc..ec261d73a 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -28,7 +28,7 @@ namespace LambdaCalculus.LocallyNameless.Untyped.Term
 @[simp, scoped grind =]
 def multiApp (f : Term Var) : List (Term Var) → Term Var
 | []      => f
-| a :: as => Term.app (multiApp f as) a
+| a :: as => multiApp (Term.app f a) as
 
 /-- A list of arguments performs a single reduction step
 
@@ -45,18 +45,23 @@ inductive ListFullBeta : List (Term Var) → List (Term Var) → Prop where
 
 variable {M M' : Term Var} {Ns Ns' : List (Term Var)}
 
+lemma multiApp_tail {N} : (M.multiApp (Ns ++ [N])) = Term.app (M.multiApp Ns) N:= by
+  induction Ns generalizing M with
+  | nil => grind
+  | cons head tail ih => rw [List.cons_append]; apply ih
+
 /-- 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]
+  induction Ns generalizing M with grind [cases LC]
 
 /-- 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
+  induction Ns generalizing M M' with grind
 
 /-- 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) :
@@ -66,12 +71,18 @@ 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
+  induction steps generalizing M <;> grind
 
 /-- 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
 
+lemma listFullBeta_cons_r {l} (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (l ++ Ns) ⭢lβᶠ (l ++ Ns')
+  := by induction l using List.reverseRecOn generalizing Ns Ns' with grind
+
+lemma listFullBeta_cons_l {l} (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (Ns ++ l) ⭢lβᶠ (Ns' ++ l)
+  := by induction h with grind
+
 set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- 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:
@@ -86,16 +97,32 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
     (∃ N', N ⭢βᶠ N' ∧ 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
+  induction Ps using List.reverseRecOn generalizing M N Q with
   | nil => grind only [cases Xi, multiApp]
-  | cons P Ps ih =>
-    generalize Heq : (M.abs.app N).multiApp Ps = Q'
-    have : ∀ P', Q'.app P' = (M.abs.app N).multiApp (P' :: Ps) := by grind
-    rw [multiApp, Heq] at h_red
+  | append_singleton Ps P ih =>
+    rw [multiApp_tail] at h_red
     cases h_red with
-    | base => cases Ps <;> grind
-    | appR => grind [→ ListFullBeta.cons]
-    | appL => grind
+    | @appL _ _ P' =>
+        right
+        right
+        left
+        refine ⟨Ps ++ [P'], listFullBeta_cons_r ?_ ?_, ?_⟩
+        all_goals grind [multiApp_tail]
+    | @appR _ _ _ _ h =>
+        specialize ih h
+        rcases ih with (_|_| ⟨Ps', h, _⟩ | _)
+        · grind [multiApp_tail]
+        · grind [multiApp_tail]
+        · right
+          right
+          left
+          refine ⟨Ps' ++ [P], listFullBeta_cons_l h ?_, ?_⟩
+          all_goals grind [multiApp_tail]
+        · grind [multiApp_tail]
+    | base =>
+        exfalso
+        induction Ps using List.reverseRecOn generalizing M N with grind [multiApp_tail]
+
 
 /-- If a term (λ M) N P₁ ... Pₙ reduces in multiple steps to Q, then either Q if of the form
 
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
index 66dd185ff..467d636a3 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
@@ -124,20 +124,25 @@ lemma sn_abs_app_multiApp [DecidableEq Var] [HasFresh Var] {Ps} {M N : Term Var}
     (sn_N : SN FullBeta N) (sn_MNPs : SN FullBeta (multiApp (M ^ N) Ps))
     (lc_N : LC N) (lc_MNPs : LC (multiApp (M ^ N) Ps)) :
     SN FullBeta (multiApp (M.abs.app N) Ps) := by
-  induction Ps with
+  induction Ps using List.reverseRecOn with
   | nil =>
     apply sn_app
     · grind [sn_abs]
     · exact sn_N
     · grind [→ steps_open_cong_abs, open_abs_lc, sn_steps]
-  | cons P Ps ih =>
+  | append_singleton Ps P ih =>
+    rw [multiApp_tail]
     apply sn_app
-    · cases lc_MNPs with grind [sn_app_left]
-    · grind [sn_app_right]
+    · rw [multiApp_tail] at *
+      cases lc_MNPs
+      grind [sn_app_left]
+    · rw [multiApp_tail] at sn_MNPs
+      grind [sn_app_right]
     · intro Q' P' hstep1 hstep2
       have ⟨M', N', Ps', h_M_red, h_N_red, h_Ps_red, h_cases⟩ := invert_abs_multiApp_mst hstep1
       rcases h_cases with h_P | ⟨h_st1, h_st2⟩
-      · cases Ps' with grind
+      · exfalso
+        induction Ps' using List.reverseRecOn generalizing M' N' with grind [multiApp_tail]
       · have innerSteps : (M ^ N).multiApp Ps ↠βᶠ (M' ^ N').multiApp Ps' := by
           trans
           · exact steps_multiApp_r h_Ps_red (by grind)
@@ -145,15 +150,15 @@ lemma sn_abs_app_multiApp [DecidableEq Var] [HasFresh Var] {Ps} {M N : Term Var}
             · apply steps_open_cong_abs M M' N N' <;> grind [open_abs_lc]
             · grind [multiApp_steps_lc]
         refine sn_steps ?_ sn_MNPs
+        rw [multiApp_tail]
         · calc ((M ^ N).multiApp Ps).app P
             _ ↠βᶠ ((M ^ N).multiApp Ps).app P' := by grind
             _ ↠βᶠ Q'.abs.app P' := redex_app_l_cong (.trans innerSteps h_st2) (by grind)
             _ ↠βᶠ Q' ^ P' := by
               rw [Relation.reflTransGen_iff_eq_or_transGen] at ⊢ innerSteps h_st2
               right
-              cases lc_MNPs
               refine Relation.TransGen.single (Xi.base (Beta.beta ?_ ?_))
-              all_goals grind only [→ step_lc_r]
+              all_goals grind
 
 end LambdaCalculus.LocallyNameless.Untyped.Term
 

From 95fb8c05f1cb03871d6090e50b525dd12b0d803a Mon Sep 17 00:00:00 2001
From: lyj <sjtu5140809011@gmail.com>
Date: Sun, 12 Jul 2026 05:07:46 +0800
Subject: [PATCH 02/10] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
index 323fa056f..cb858529d 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
@@ -71,8 +71,7 @@ lemma semanticMap_saturated (τ : Ty Base) : @Saturated Var (semanticMap τ) :=
     · grind [sn_app_left (Var := Var) (N := fvar <| fresh {})]
     · grind
     · intro M N P _ _ _ s _
-      have := ih₂.multiApp M N (P ++ [s])
-      grind [multiApp_tail]
+      grind [ih₂.multiApp M N (P ++ [s]), multiApp_tail]
 
 /-- The `entailsContext` predicate ensures that each variable in the context
     is mapped to a term in the corresponding semantic map. -/

From c5741bcc8c15ad85015a2824710cc9b939f95ce8 Mon Sep 17 00:00:00 2001
From: lyj <sjtu5140809011@gmail.com>
Date: Sun, 12 Jul 2026 05:08:06 +0800
Subject: [PATCH 03/10] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 .../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 ec261d73a..290669fd6 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -28,7 +28,7 @@ namespace LambdaCalculus.LocallyNameless.Untyped.Term
 @[simp, scoped grind =]
 def multiApp (f : Term Var) : List (Term Var) → Term Var
 | []      => f
-| a :: as => multiApp (Term.app f a) as
+| a :: as => multiApp (app f a) as
 
 /-- A list of arguments performs a single reduction step
 

From d77ac7afe7da30bf9af86663d729d2f62251ae91 Mon Sep 17 00:00:00 2001
From: lyj <sjtu5140809011@gmail.com>
Date: Sun, 12 Jul 2026 05:08:22 +0800
Subject: [PATCH 04/10] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 .../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 290669fd6..1e15b9706 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -45,7 +45,7 @@ inductive ListFullBeta : List (Term Var) → List (Term Var) → Prop where
 
 variable {M M' : Term Var} {Ns Ns' : List (Term Var)}
 
-lemma multiApp_tail {N} : (M.multiApp (Ns ++ [N])) = Term.app (M.multiApp Ns) N:= by
+lemma multiApp_tail {N} : (M.multiApp (Ns ++ [N])) = (M.multiApp Ns).app  N:= by
   induction Ns generalizing M with
   | nil => grind
   | cons head tail ih => rw [List.cons_append]; apply ih

From e9c289905a2e8ff68bfb515596836813c7859812 Mon Sep 17 00:00:00 2001
From: lyj <sjtu5140809011@gmail.com>
Date: Sun, 12 Jul 2026 05:08:37 +0800
Subject: [PATCH 05/10] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 1e15b9706..6f407ca46 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -77,8 +77,8 @@ 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
 
-lemma listFullBeta_cons_r {l} (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (l ++ Ns) ⭢lβᶠ (l ++ Ns')
-  := by induction l using List.reverseRecOn generalizing Ns Ns' with grind
+lemma listFullBeta_cons_r {l} (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (l ++ Ns) ⭢lβᶠ (l ++ Ns') := by
+  induction l using List.reverseRecOn generalizing Ns Ns' with grind
 
 lemma listFullBeta_cons_l {l} (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (Ns ++ l) ⭢lβᶠ (Ns' ++ l)
   := by induction h with grind

From eb50dd908e0f927889bde31a1439f0bb24a26f54 Mon Sep 17 00:00:00 2001
From: lyj <sjtu5140809011@gmail.com>
Date: Sun, 12 Jul 2026 05:08:48 +0800
Subject: [PATCH 06/10] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 6f407ca46..68f849b99 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -80,8 +80,8 @@ lemma steps_multiApp_r (steps : Ns ↠lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns
 lemma listFullBeta_cons_r {l} (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (l ++ Ns) ⭢lβᶠ (l ++ Ns') := by
   induction l using List.reverseRecOn generalizing Ns Ns' with grind
 
-lemma listFullBeta_cons_l {l} (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (Ns ++ l) ⭢lβᶠ (Ns' ++ l)
-  := by induction h with grind
+lemma listFullBeta_cons_l {l} (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (Ns ++ l) ⭢lβᶠ (Ns' ++ l) := by
+  induction h with grind
 
 set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- If a term (λ M) N P_1 ... P_n reduces in a single step to Q, then

From ff6f03ebe2110ea45b1e40ce9069291546263e36 Mon Sep 17 00:00:00 2001
From: lyj <sjtu5140809011@gmail.com>
Date: Sun, 12 Jul 2026 05:09:17 +0800
Subject: [PATCH 07/10] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 68f849b99..5cce8ae92 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -102,26 +102,13 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
   | append_singleton Ps P ih =>
     rw [multiApp_tail] at h_red
     cases h_red with
-    | @appL _ _ P' =>
-        right
-        right
-        left
-        refine ⟨Ps ++ [P'], listFullBeta_cons_r ?_ ?_, ?_⟩
-        all_goals grind [multiApp_tail]
-    | @appR _ _ _ _ h =>
-        specialize ih h
-        rcases ih with (_|_| ⟨Ps', h, _⟩ | _)
-        · grind [multiApp_tail]
-        · grind [multiApp_tail]
-        · right
-          right
-          left
-          refine ⟨Ps' ++ [P], listFullBeta_cons_l h ?_, ?_⟩
-          all_goals grind [multiApp_tail]
-        · grind [multiApp_tail]
-    | base =>
-        exfalso
-        induction Ps using List.reverseRecOn generalizing M N with grind [multiApp_tail]
+    | @appL _ _ P' _ P_P' =>
+      have : (Ps ++ [P]) ⭢lβᶠ Ps ++ [P'] := by apply listFullBeta_cons_r (.step P_P' ?_) <;> grind
+      grind [multiApp_tail]
+    | appR _ h =>
+      have {Ps'} (h : Ps ⭢lβᶠ Ps') : (Ps ++ [P]) ⭢lβᶠ Ps' ++ [P] := listFullBeta_cons_l h (by grind)
+      grind [multiApp_tail]
+    | base => induction Ps using List.reverseRecOn with grind [multiApp_tail]
 
 
 /-- If a term (λ M) N P₁ ... Pₙ reduces in multiple steps to Q, then either Q if of the form

From 44c02fcb638ad77564524ff336b54e265bb51a86 Mon Sep 17 00:00:00 2001
From: lyj <sjtu5140809011@gmail.com>
Date: Sun, 12 Jul 2026 05:09:34 +0800
Subject: [PATCH 08/10] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
index 467d636a3..d2dab230a 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
@@ -141,8 +141,7 @@ lemma sn_abs_app_multiApp [DecidableEq Var] [HasFresh Var] {Ps} {M N : Term Var}
     · intro Q' P' hstep1 hstep2
       have ⟨M', N', Ps', h_M_red, h_N_red, h_Ps_red, h_cases⟩ := invert_abs_multiApp_mst hstep1
       rcases h_cases with h_P | ⟨h_st1, h_st2⟩
-      · exfalso
-        induction Ps' using List.reverseRecOn generalizing M' N' with grind [multiApp_tail]
+      · induction Ps' using List.reverseRecOn with grind [multiApp_tail]
       · have innerSteps : (M ^ N).multiApp Ps ↠βᶠ (M' ^ N').multiApp Ps' := by
           trans
           · exact steps_multiApp_r h_Ps_red (by grind)

From 95ac53667346e9de5e30bb22368aff0404fc64c4 Mon Sep 17 00:00:00 2001
From: lyj <sjtu5140809011@gmail.com>
Date: Sun, 12 Jul 2026 05:09:51 +0800
Subject: [PATCH 09/10] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
index d2dab230a..ea45ee0e8 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
@@ -133,11 +133,8 @@ lemma sn_abs_app_multiApp [DecidableEq Var] [HasFresh Var] {Ps} {M N : Term Var}
   | append_singleton Ps P ih =>
     rw [multiApp_tail]
     apply sn_app
-    · rw [multiApp_tail] at *
-      cases lc_MNPs
-      grind [sn_app_left]
-    · rw [multiApp_tail] at sn_MNPs
-      grind [sn_app_right]
+    · grind [cases LC, multiApp_tail, sn_app_left]
+    · grind [multiApp_tail, sn_app_right]
     · intro Q' P' hstep1 hstep2
       have ⟨M', N', Ps', h_M_red, h_N_red, h_Ps_red, h_cases⟩ := invert_abs_multiApp_mst hstep1
       rcases h_cases with h_P | ⟨h_st1, h_st2⟩

From cc288fa29edc8ba44ae75b2467b5affa27b47cba Mon Sep 17 00:00:00 2001
From: lyj <sjtu5140809011@gmail.com>
Date: Sun, 12 Jul 2026 05:58:13 +0800
Subject: [PATCH 10/10] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 5cce8ae92..877390646 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -77,10 +77,10 @@ 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
 
-lemma listFullBeta_cons_r {l} (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (l ++ Ns) ⭢lβᶠ (l ++ Ns') := by
+lemma listFullBeta_cons_r (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (l ++ Ns) ⭢lβᶠ (l ++ Ns') := by
   induction l using List.reverseRecOn generalizing Ns Ns' with grind
 
-lemma listFullBeta_cons_l {l} (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (Ns ++ l) ⭢lβᶠ (Ns' ++ l) := by
+lemma listFullBeta_cons_l (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (Ns ++ l) ⭢lβᶠ (Ns' ++ l) := by
   induction h with grind
 
 set_option linter.tacticAnalysis.verifyGrindOnly false in