diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
index 36c6c816d..bd329e28a 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
@@ -151,9 +151,13 @@ 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
+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