lengyijun · Jun 24, 2026 · Oct 11, 2026 · Oct 11, 2026
@@ -121,14 +121,14 @@ lemma redex_abs_close {x : Var} (step : M ↠βᶠ M') : (M⟦0 ↜ x⟧.abs ↠
 theorem step_abs_cong (xs : Finset Var) (cofin : ∀ x ∉ xs, (M ^ fvar x) ⭢βᶠ (M' ^ fvar x)) :
     M.abs ⭢βᶠ M'.abs := by
   have ⟨fresh, _⟩ := fresh_exists <| free_union [fv] Var
-  rw [open_close fresh M 0 ?_, open_close fresh M' 0 ?_]
+  rw [open_closeRec fresh M 0 ?_, open_closeRec fresh M' 0 ?_]
   all_goals grind [step_abs_close]
 
 /-- Multiple reduction of opening implies multiple reduction of abstraction. -/
 theorem redex_abs_cong (xs : Finset Var) (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠βᶠ (M' ^ fvar x)) :
     M.abs ↠βᶠ M'.abs := by
   have ⟨fresh, _⟩ := fresh_exists <| free_union [fv] Var
-  rw [open_close fresh M 0 ?_, open_close fresh M' 0 ?_]
+  rw [open_closeRec fresh M 0 ?_, open_closeRec fresh M' 0 ?_]
   all_goals grind [redex_abs_close]
 
 /- Reduction is preserved when opening with a locally closed term. -/

@@ -87,7 +87,7 @@ lemma stronglyCommute_eta_beta : StronglyCommute (@FullEta Var) FullBeta := by
       · cases h_beta with
         | refl => grind [open_close]
         | single => exact .single (Xi.abs {w} (by grind [FullBeta.redex_subst_cong]))
-      · rw [open_close w N 0 (by grind)]
+      · rw [open_closeRec w N 0 (by grind)]
         exact FullEta.redex_abs_close h_eta
 
 open Commute in

@@ -111,7 +111,7 @@ theorem redex_abs_cong {M M' : Term Var} (xs : Finset Var)
     (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠ηᶠ M' ^ fvar x) :
     M.abs ↠ηᶠ M'.abs := by
     have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
-    rw [open_close x M 0, open_close x M' 0]
+    rw [open_closeRec x M 0, open_closeRec x M' 0]
     all_goals grind [redex_abs_close (x := x) (cofin x ?_)]
 
 /- `t ⭢ηᶠ t'` implies `s[x := t] ↠ηᶠ s[x := t']`. -/
@@ -154,7 +154,7 @@ open Relation in
 lemma close_eta_steps (hx_M : x ∉ M.fv) (st_M : ReflGen FullEta (M ^ fvar x) N) :
     ReflGen FullEta M.abs (N ^* x).abs := by
   cases st_M with
-  | refl => rw [←open_close_var x M hx_M]
+  | refl => rw [←open_close x M hx_M]
   | single st =>
     exact .single (Xi.abs {x} (by grind [step_subst_cong_l]))
 

@@ -110,7 +110,7 @@ lemma Leftmost.steps_abs_cong (xs : Finset Var)
     (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠ℓ (M' ^ fvar x)) (lc : LC (abs M)) :
     abs M ↠ℓ abs M' := by
   have ⟨w, _⟩ := fresh_exists <| free_union [fv] Var
-  rw [open_close w M 0 (by grind), open_close w M' 0 (by grind)]
+  rw [open_closeRec w M 0 (by grind), open_closeRec w M' 0 (by grind)]
   have hstep := cofin w (by grind)
   have hlc := beta_lc lc (.fvar w)
   exact steps_abs_close hstep hlc

@@ -29,17 +29,17 @@ theorem subst_fresh (x : Var) (t sub : Term Var) (nmem : x ∉ t.fv) : t[x := su
   induction t <;> grind
 
 /- Opening and closing are inverses. -/
-lemma open_close (x : Var) (t : Term Var) (k : ℕ) (nmem : x ∉ t.fv) : t = t⟦k ↝ fvar x⟧⟦k ↜ x⟧ := by
-  induction t generalizing k <;> grind
+lemma open_closeRec (x : Var) (t : Term Var) (k : ℕ) (nmem : x ∉ t.fv) :
+  t = t⟦k ↝ fvar x⟧⟦k ↜ x⟧ := by induction t generalizing k <;> grind
 
 /-- Specializes `open_close` to the first closing. -/
-lemma open_close_var (x : Var) (t : Term Var) (nmem : x ∉ t.fv) : t = (t ^ fvar x) ^* x :=
-  open_close x t 0 nmem
+lemma open_close (x : Var) (t : Term Var) (nmem : x ∉ t.fv) : t = (t ^ fvar x) ^* x :=
+  open_closeRec x t 0 nmem
 
 /-- Opening is injective. -/
 lemma open_injective (x : Var) (M M') (free_M : x ∉ M.fv) (free_M' : x ∉ M'.fv)
     (eq : M ^ fvar x = M' ^ fvar x) : M = M' := by
-  grind [open_close x M 0 free_M, open_close x M' 0 free_M']
+  grind [open_closeRec x M 0 free_M, open_closeRec x M' 0 free_M']
 
 /-- Opening and closing are associative for nonclashing free variables. -/
 lemma swap_open_fvar_close (k n : ℕ) (x y : Var) (m : Term Var) (neq₁ : k ≠ n) (neq₂ : x ≠ y) :
@@ -140,7 +140,7 @@ lemma close_openRec_to_subst (m n : Term Var) (x : Var) (k : ℕ) (m_lc : LC m)
   | abs xs t =>
     have ⟨x', _⟩ := fresh_exists <| free_union [fv] Var
     simp only [closeRec_abs, openRec_abs, subst_abs]
-    rw [open_close x' (t⟦k+1 ↜ x⟧⟦k+1 ↝ n⟧) 0, open_close x' (t[x := n]) 0]
+    rw [open_closeRec x' (t⟦k+1 ↜ x⟧⟦k+1 ↝ n⟧) 0, open_closeRec x' (t[x := n]) 0]
     · grind [swap_open, =_ swap_open_fvar_close]
     · grind [subst_preserve_not_fvar]
     · grind [open_preserve_not_fvar]
@@ -150,10 +150,14 @@ lemma close_openRec_to_subst (m n : Term Var) (x : Var) (k : ℕ) (m_lc : LC m)
 lemma close_open_to_subst (m n : Term Var) (x : Var) (m_lc : LC m) (n_lc : LC n) :
     (m ^* x) ^ n = m[x := n] := close_openRec_to_subst m n x 0 m_lc n_lc
 
-/-- Closing and opening are inverses. -/
-lemma close_open (x : Var) (t : Term Var) (k : ℕ) (t_lc : LC t) : t⟦k ↜ x⟧⟦k ↝ fvar x⟧ = t := by
+/-- CloseRec and openRec are inverses. -/
+lemma close_openRec (x : Var) (t : Term Var) (k : ℕ) (t_lc : LC t) : t⟦k ↜ x⟧⟦k ↝ fvar x⟧ = t := by
   grind [subst_refl]
 
+/-- Closing and opening are inverses. -/
+lemma close_open (x : Var) (t : Term Var) (t_lc : LC t) : (t ^* x) ^ fvar x = t :=
+  close_openRec x t 0 t_lc
+
 end LambdaCalculus.LocallyNameless.Untyped.Term
 
 end Cslib
@@ -376,7 +376,7 @@ lemma StandardSeq.abs_cong (xs : Finset Var)
   have ⟨n, hseq⟩ := cofin w (by grind)
   have hlc := beta_lc lc (.fvar w)
   have habs : StandardSeq n (abs M) (abs M') := by
-    rw [open_close w M 0 (by grind), open_close w M' 0 (by grind)]
+    rw [open_closeRec w M 0 (by grind), open_closeRec w M' 0 (by grind)]
     exact hseq.abs_close hlc
   exact ⟨n, habs⟩