From 259db84e4ffb76cdf58eaf4b4bb660f91a468b05 Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Tue, 22 Sep 2026 07:50:14 +0800
Subject: [PATCH] feat(LocallyNameless): new theorems in FullBetaEta

    1. The old multi-step lemmas

    redex_app_l_cong and redex_app_r_cong

    become

    single-step: step_app_l_cong / step_app_r_cong
    multi-step: steps_app_l_cong / steps_app_r_cong

    2. new theorems:

      step_fv
      steps_fv
      step_subst_cong_l
      steps_subst_cong_l
---
 .../LocallyNameless/Untyped/FullBetaEta.lean  | 55 ++++++++++++++-----
 1 file changed, 40 insertions(+), 15 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEta.lean
index e847f97de2..26e7f5e8a4 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEta.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEta.lean
@@ -37,23 +37,48 @@ abbrev FullBetaEta : Term Var → Term Var → Prop := FullBeta ⊔ FullEta
 
 namespace FullBetaEta
 
-theorem redex_app_l_cong (redex : M ↠βηᶠ M') (lc_N : LC N) : app M N ↠βηᶠ app M' N := by
-  induction redex with
+variable {M M' N N' : Term Var}
+
+theorem step_app_l_cong (step : M ⭢βηᶠ M') (h_lc : LC N) : app M N ⭢βηᶠ app M' N := by
+    rcases step with h | h
+    · exact join_inl (h.appR h_lc)
+    · exact join_inr (h.appR h_lc)
+
+theorem step_app_r_cong (step : M ⭢βηᶠ M') (h_lc : LC N) : app N M ⭢βηᶠ app N M' := by
+    rcases step with h | h
+    · exact join_inl (h.appL h_lc)
+    · exact join_inr (h.appL h_lc)
+
+theorem steps_app_l_cong (steps : M ↠βηᶠ M') (h_lc : LC N) : app M N ↠βηᶠ app M' N := by
+  induction steps with
+  | refl => grind
+  | tail _ h ih => exact ih.tail (step_app_l_cong h h_lc)
+
+theorem steps_app_r_cong (steps : M ↠βηᶠ M') (h_lc : LC N) : app N M ↠βηᶠ app N M' := by
+  induction steps with
   | refl => grind
-  | tail _ h ih =>
-    refine .tail ih ?_
-    rcases h with h | h
-    · exact join_inl (h.appR lc_N)
-    · exact join_inr (h.appR lc_N)
-
-theorem redex_app_r_cong (redex : M ↠βηᶠ M') (lc_N : LC N) : app N M ↠βηᶠ app N M' := by
-  induction redex with
+  | tail _ h ih => exact ih.tail (step_app_r_cong h h_lc)
+
+variable [HasFresh Var] [DecidableEq Var]
+
+lemma step_fv (step : M ⭢βηᶠ M') : M'.fv ⊆ M.fv := by
+    cases step with
+    | inl h => grind [FullBeta.step_not_fv h]
+    | inr h => grind [FullEta.step_not_fv h]
+
+lemma steps_fv (steps : M ↠βηᶠ M') : M'.fv ⊆ M.fv := by
+  induction steps with
   | refl => grind
-  | tail _ h ih =>
-    refine .tail ih ?_
-    rcases h with h | h
-    · exact join_inl (h.appL lc_N)
-    · exact join_inr (h.appL lc_N)
+  | tail _ step _ => grind [step_fv step]
+
+lemma step_subst_cong_l (x : Var) (step : M ⭢βηᶠ M') (h_lc : LC N) : M[x := N] ⭢βηᶠ M'[x := N] := by
+  cases step with
+  | inl h => exact Or.inl (FullBeta.redex_subst_cong_lc _ _ _ _ h h_lc)
+  | inr h => exact Or.inr (FullEta.step_subst_cong_l _ _ _  h h_lc)
+
+lemma steps_subst_cong_l (x : Var) (steps : M ↠βηᶠ M') (h_lc : LC N) :
+    M[x := N] ↠βηᶠ M'[x := N] := by
+  induction steps with grind [step_subst_cong_l]
 
 end FullBetaEta