From 6b8aae0a93562c8275356b5fbe73139ca8d7d6f4 Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Sun, 26 Jul 2026 08:40:14 +0800
Subject: [PATCH] fix: remove grind attr from Xi.step_lc_r

---
 .../LambdaCalculus/LocallyNameless/Untyped/Congruence.lean       | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Congruence.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Congruence.lean
index 9694ecfd29..d0c2c43b1f 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Congruence.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Congruence.lean
@@ -38,7 +38,6 @@ namespace Xi
 variable {R : Term Var → Term Var → Prop} {M N : Term Var}
 
 /-- The right side of a congruence step is locally closed. -/
-@[scoped grind →]
 lemma step_lc_r (hR : ∀ {M' N'}, R M' N' → LC N') (step : Xi R M N) : LC N := by
   induction step with
   | base h => exact hR h