diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean
index 2231d2b08..eee34a2a9 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean
@@ -45,6 +45,7 @@ lemma step_lc_r (step : M ⭢ηᶠ M') : LC M' := by
   grind
 
 /-- The left side of an η-reduction is locally closed. -/
+@[scoped grind →]
 lemma step_lc_l [HasFresh Var] (step : M ⭢ηᶠ M') : LC M := by
   induction step with
   | base h_e => cases h_e with | eta => apply LC.abs ∅; grind
@@ -52,6 +53,9 @@ lemma step_lc_l [HasFresh Var] (step : M ⭢ηᶠ M') : LC M := by
   | appR lc_Z _ ih => exact LC.app ih lc_Z
   | @abs M' _ xs _ ih => exact LC.abs xs M' ih
 
+lemma steps_lc_l [HasFresh Var] (step : M ↠ηᶠ M') (h : LC M') : LC M := by
+  induction step with grind
+
 /-- Left congruence rule for application in multiple reduction. -/
 theorem redex_app_l_cong (redex : M ↠ηᶠ M') (lc_N : LC N) : app M N ↠ηᶠ app M' N := by
   induction redex <;> grind