From c90672330e479e115918c5b3d445b7af435cffdd Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Wed, 2 Sep 2026 13:19:55 +0800
Subject: [PATCH 1/7] refactor(Locallynameless): abbrev multiApp = `List.foldl
 app`

Replace the recursive multiApp definition with List.foldl app
Remove the now-unnecessary multiApp_tail lemma and adapt proofs to List.foldl_concat
Make semanticMap_saturated use explicit grind only lemmas for the new multiApp representation
New theorems : multiapp_openRec and multiapp_fv
---
 .../LocallyNameless/Stlc/StrongNorm.lean      |  3 +-
 .../LocallyNameless/Untyped/MultiApp.lean     | 31 +++++++++++--------
 .../LocallyNameless/Untyped/StrongNorm.lean   | 13 +++++---
 3 files changed, 28 insertions(+), 19 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
index 6b1e8f387f..03cdfe2d80 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean
@@ -66,7 +66,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 (P ++ [s]), multiApp_tail]
+      grind only [semanticMap, = List.foldl_append, = List.foldl_cons, usr Set.mem_ofPred_eq,
+                  = List.foldl_nil, ih₂.multiApp M N (P ++ [s])]
 
 /-- 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 509b4a52c6..3b03304e69 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -26,9 +26,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ₙ). -/
 @[simp, scoped grind =]
-def multiApp (f : Term Var) : List (Term Var) → Term Var
-| []      => f
-| a :: as => multiApp (app f a) as
+abbrev multiApp (f : Term Var) (Ns : List (Term Var)) := Ns.foldl app f
 
 /-- A list of arguments performs a single reduction step
 
@@ -45,11 +43,6 @@ 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])) = (M.multiApp Ns).app  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 ←]
@@ -80,6 +73,17 @@ 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 multiapp_openRec {i} :
+   (multiApp M Ns)⟦i ↝ M'⟧ = multiApp (M⟦i ↝ M'⟧) (Ns.map (openRec i M')) := by
+  induction Ns generalizing M with
+  | nil => grind
+  | cons head tail ih => grind [@ih (M.app head)]
+
+lemma multiapp_fv [DecidableEq Var] : (multiApp M Ns).fv = (Ns.map fv).foldl Union.union M.fv := by
+  induction Ns generalizing M with
+  | nil => grind
+  | cons head tail ih => grind [@ih (M.app head)]
+
 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
 
@@ -101,17 +105,18 @@ 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 using List.reverseRecOn generalizing M N Q with
-  | nil => grind only [cases Xi, multiApp]
+  | nil => grind [cases Xi]
   | append_singleton Ps P ih =>
-    rw [multiApp_tail] at h_red
+    unfold multiApp at h_red
+    rw [List.foldl_concat] at h_red
     cases h_red with
     | @appL _ _ P' _ P_P' =>
       have : (Ps ++ [P]) ⭢lβᶠ Ps ++ [P'] := by apply listFullBeta_cons_r (.step P_P' ?_) <;> grind
-      grind [multiApp_tail]
+      grind
     | 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]
+      grind
+    | base => induction Ps using List.reverseRecOn with grind
 
 
 /-- 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 b54be7de11..0bbe76f0a2 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
@@ -129,16 +129,18 @@ lemma sn_abs_app_multiApp [DecidableEq Var] [HasFresh Var] {Ps} {M N : Term Var}
     · exact sn_N
     · grind [→ steps_open_cong_abs, open_abs_lc, sn_steps]
   | append_singleton Ps P ih =>
-    rw [multiApp_tail]
+    unfold multiApp
+    rw [List.foldl_concat]
     apply sn_app
-    · rw [multiApp_tail] at sn_MNPs lc_MNPs
+    · unfold multiApp at sn_MNPs lc_MNPs
+      rw [List.foldl_concat] at sn_MNPs lc_MNPs
       cases lc_MNPs
       grind [sn_app_left]
-    · grind [multiApp_tail, sn_app_right]
+    · 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⟩
-      · induction Ps' using List.reverseRecOn with grind [multiApp_tail]
+      · induction Ps' using List.reverseRecOn with grind
       · have innerSteps : (M ^ N).multiApp Ps ↠βᶠ (M' ^ N').multiApp Ps' := by
           trans
           · exact steps_multiApp_r h_Ps_red (by grind)
@@ -146,7 +148,8 @@ 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]
+        unfold multiApp
+        rw [List.foldl_concat]
         · 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)

From 85df5fd4a5d95e2ddb138dc9de5066cd385b0424 Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Wed, 2 Sep 2026 14:05:59 +0800
Subject: [PATCH 2/7] feat: `ListFullBeta` context lemmas

Rename `listFullBeta_cons_r/l` to `listFullBeta_concat_r/l` to reflect their general concatenation behavior.
Add specialized `cons` lemmas for reducing the head term or the tail list.
---
 .../LocallyNameless/Untyped/MultiApp.lean        | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 3b03304e69..d088c1a481 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -84,12 +84,20 @@ lemma multiapp_fv [DecidableEq Var] : (multiApp M Ns).fv = (Ns.map fv).foldl Uni
   | nil => grind
   | cons head tail ih => grind [@ih (M.app head)]
 
-lemma listFullBeta_cons_r (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (l ++ Ns) ⭢lβᶠ (l ++ Ns') := by
+lemma listFullBeta_concat_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 (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (Ns ++ l) ⭢lβᶠ (Ns' ++ l) := by
+lemma listFullBeta_concat_l (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (Ns ++ l) ⭢lβᶠ (Ns' ++ l) := by
   induction h with grind
 
+lemma listFullBeta_cons_r (h : Ns ↠lβᶠ Ns') (h_lc : LC M) : (M :: Ns) ↠lβᶠ (M :: Ns') := by
+  induction h with grind
+
+lemma listFullBeta_cons_l (h : M ↠βᶠ M') (h_lc : ∀ M ∈ Ns, LC M) : (M :: Ns) ↠lβᶠ (M' :: Ns) := by
+  induction h with
+  | refl => grind
+  | tail _ h ih => exact .tail ih (.step h h_lc)
+
 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:
@@ -111,10 +119,10 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
     rw [List.foldl_concat] at h_red
     cases h_red with
     | @appL _ _ P' _ P_P' =>
-      have : (Ps ++ [P]) ⭢lβᶠ Ps ++ [P'] := by apply listFullBeta_cons_r (.step P_P' ?_) <;> grind
+      have : (Ps ++ [P]) ⭢lβᶠ Ps ++ [P'] := by apply listFullBeta_concat_r (.step P_P' ?_) <;> grind
       grind
     | appR _ h =>
-      have {Ps'} (h : Ps ⭢lβᶠ Ps') : (Ps ++ [P]) ⭢lβᶠ Ps' ++ [P] := listFullBeta_cons_l h (by grind)
+      have {Ps'} (h : Ps ⭢lβᶠ Ps') : (Ps ++ [P]) ⭢lβᶠ Ps' ++ [P] := listFullBeta_concat_l h (by grind)
       grind
     | base => induction Ps using List.reverseRecOn with grind
 

From 1482228848f7ba1d06803c10ef6fe7cb3a69521e Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Wed, 2 Sep 2026 14:12:12 +0800
Subject: [PATCH 3/7] Add `multiApp` congruence lemmas for union reductions
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Add `step_multiApp_l_union` to lift a single `(Xi R1 ⊔ Xi R2)` reduction through a multi-application.
Add `steps_multiApp_l_union` for the corresponding reflexive-transitive closure.
Use the new single-step lemma to simplify the proof of the multi-step result.
---
 .../LocallyNameless/Untyped/MultiApp.lean        | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index d088c1a481..31c0fcfc45 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -64,6 +64,22 @@ lemma steps_multiApp_l (steps : M ↠βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) :
     M.multiApp Ns ↠βᶠ M'.multiApp Ns := by
   induction steps <;> grind
 
+lemma step_multiApp_l_union {R1 R2} (step : (Xi R1 ⊔ Xi R2) M M') (lc_Ns : ∀ N ∈ Ns, LC N) :
+   (Xi R1 ⊔ Xi R2) (multiApp M Ns) (multiApp M' Ns) := by
+  induction Ns generalizing M M' with
+  | nil => grind
+  | cons head tail ih =>
+      apply ih ?_ (by grind)
+      cases step with
+        | inl h =>  left; grind
+        | inr h =>  right; grind
+
+lemma steps_multiApp_l_union {R1 R2}
+  (steps : Relation.ReflTransGen (Xi R1 ⊔ Xi R2) M M')
+  (lc_Ns : ∀ N ∈ Ns, LC N) :
+   Relation.ReflTransGen (Xi R1 ⊔ Xi R2) (multiApp M Ns) (multiApp M' Ns) := by
+  induction steps <;> grind [step_multiApp_l_union]
+
 /-- 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

From 4768f4dbfbcc0b89b534201399668369cc31e57d Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Wed, 2 Sep 2026 14:23:24 +0800
Subject: [PATCH 4/7] format

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 31c0fcfc45..67c98fd722 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -100,10 +100,12 @@ lemma multiapp_fv [DecidableEq Var] : (multiApp M Ns).fv = (Ns.map fv).foldl Uni
   | nil => grind
   | cons head tail ih => grind [@ih (M.app head)]
 
-lemma listFullBeta_concat_r (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (l ++ Ns) ⭢lβᶠ (l ++ Ns') := by
+lemma listFullBeta_concat_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_concat_l (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (Ns ++ l) ⭢lβᶠ (Ns' ++ l) := by
+lemma listFullBeta_concat_l (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) :
+  (Ns ++ l) ⭢lβᶠ (Ns' ++ l) := by
   induction h with grind
 
 lemma listFullBeta_cons_r (h : Ns ↠lβᶠ Ns') (h_lc : LC M) : (M :: Ns) ↠lβᶠ (M :: Ns') := by
@@ -138,8 +140,8 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
       have : (Ps ++ [P]) ⭢lβᶠ Ps ++ [P'] := by apply listFullBeta_concat_r (.step P_P' ?_) <;> grind
       grind
     | appR _ h =>
-      have {Ps'} (h : Ps ⭢lβᶠ Ps') : (Ps ++ [P]) ⭢lβᶠ Ps' ++ [P] := listFullBeta_concat_l h (by grind)
-      grind
+    have {Ps'} (h : Ps ⭢lβᶠ Ps') : (Ps ++ [P]) ⭢lβᶠ Ps' ++ [P] := listFullBeta_concat_l h (by grind)
+    grind
     | base => induction Ps using List.reverseRecOn with grind
 
 

From a5f06ae75c3c3189628ef972938d9db3c22b528a Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Sun, 11 Oct 2026 08:23:45 +0800
Subject: [PATCH 5/7] multiApp_lc: 32.825737s => 0.411336s

---
 .../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 67c98fd722..442d49f873 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -47,7 +47,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
-  induction Ns generalizing M with grind [cases LC]
+  induction Ns using List.reverseRecOn with grind [cases LC]
 
 /-- Just like ordinary beta reduction, the left-hand side
     of a multi-application step is locally closed -/

From a0209a3581c8321204bc20fcf05fe919f02ad255 Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Sun, 11 Oct 2026 08:28:27 +0800
Subject: [PATCH 6/7] concat => append

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index 442d49f873..b29e3191c1 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -100,11 +100,11 @@ lemma multiapp_fv [DecidableEq Var] : (multiApp M Ns).fv = (Ns.map fv).foldl Uni
   | nil => grind
   | cons head tail ih => grind [@ih (M.app head)]
 
-lemma listFullBeta_concat_r (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) :
+lemma listFullBeta_append_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_concat_l (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) :
+lemma listFullBeta_append_l (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) :
   (Ns ++ l) ⭢lβᶠ (Ns' ++ l) := by
   induction h with grind
 
@@ -137,10 +137,10 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
     rw [List.foldl_concat] at h_red
     cases h_red with
     | @appL _ _ P' _ P_P' =>
-      have : (Ps ++ [P]) ⭢lβᶠ Ps ++ [P'] := by apply listFullBeta_concat_r (.step P_P' ?_) <;> grind
+      have : (Ps ++ [P]) ⭢lβᶠ Ps ++ [P'] := by apply listFullBeta_append_r (.step P_P' ?_) <;> grind
       grind
     | appR _ h =>
-    have {Ps'} (h : Ps ⭢lβᶠ Ps') : (Ps ++ [P]) ⭢lβᶠ Ps' ++ [P] := listFullBeta_concat_l h (by grind)
+    have {Ps'} (h : Ps ⭢lβᶠ Ps') : (Ps ++ [P]) ⭢lβᶠ Ps' ++ [P] := listFullBeta_append_l h (by grind)
     grind
     | base => induction Ps using List.reverseRecOn with grind
 

From 1c4ed24366ea82558b030192221c412b712b3aff Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Sun, 11 Oct 2026 08:39:17 +0800
Subject: [PATCH 7/7] simp only [List.foldl_concat]

---
 .../LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean | 3 +--
 .../LocallyNameless/Untyped/StrongNorm.lean              | 9 +++------
 2 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
index b29e3191c1..6737deb297 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean
@@ -133,8 +133,7 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
   induction Ps using List.reverseRecOn generalizing M N Q with
   | nil => grind [cases Xi]
   | append_singleton Ps P ih =>
-    unfold multiApp at h_red
-    rw [List.foldl_concat] at h_red
+    simp only [List.foldl_concat] at h_red
     cases h_red with
     | @appL _ _ P' _ P_P' =>
       have : (Ps ++ [P]) ⭢lβᶠ Ps ++ [P'] := by apply listFullBeta_append_r (.step P_P' ?_) <;> grind
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
index 0bbe76f0a2..1654c8d5d2 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean
@@ -129,11 +129,9 @@ lemma sn_abs_app_multiApp [DecidableEq Var] [HasFresh Var] {Ps} {M N : Term Var}
     · exact sn_N
     · grind [→ steps_open_cong_abs, open_abs_lc, sn_steps]
   | append_singleton Ps P ih =>
-    unfold multiApp
-    rw [List.foldl_concat]
+    simp only [List.foldl_concat]
     apply sn_app
-    · unfold multiApp at sn_MNPs lc_MNPs
-      rw [List.foldl_concat] at sn_MNPs lc_MNPs
+    · simp only [List.foldl_concat] at sn_MNPs lc_MNPs
       cases lc_MNPs
       grind [sn_app_left]
     · grind [sn_app_right]
@@ -148,8 +146,7 @@ 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
-        unfold multiApp
-        rw [List.foldl_concat]
+        simp only [List.foldl_concat]
         · 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)