From e7935cdc3b06d449de2f4e44d18711e8f19b3f99 Mon Sep 17 00:00:00 2001 From: lengyijun Date: Fri, 26 Jun 2026 13:43:16 +0800 Subject: [PATCH] feat(LocallyNameless/Untyped): FullEta.steps_open_cong_l --- .../LambdaCalculus/LocallyNameless/Untyped/FullEta.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean index 2231d2b08..6250d4e57 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean @@ -156,6 +156,13 @@ lemma steps_open_cong_r {s t t' : Term Var} (lc_s : LC s.abs) (lc_t : LC t) (ste case refl => rfl case head _ _ st _ ih => exact .trans (step_open_cong_r lc_s lc_t st) (ih (step_lc_r st)) +theorem steps_open_cong_l {s s' t : Term Var} (xs : Finset Var) + (h : ∀ x ∉ xs, (s ^ fvar x) ↠ηᶠ (s' ^ fvar x)) (h_lc : LC t) : + (s ^ t) ↠ηᶠ (s' ^ t) := by + have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var + rw [Term.subst_intro x _ s (by grind), Term.subst_intro x _ s' (by grind)] + exact steps_subst_cong_l _ _ _ (h x (by grind)) h_lc + /- Closing a sequence of η-reduction steps over a fresh variable preserves the steps. -/ open Relation in lemma close_eta_steps (hx_M : x ∉ M.fv) (st_M : ReflGen FullEta (M ^ fvar x) N) :