diff --git a/src/Lean/Meta/Tactic/Grind/Propagate.lean b/src/Lean/Meta/Tactic/Grind/Propagate.lean
index 14a3a786ef84..42d1135a14f0 100644
--- a/src/Lean/Meta/Tactic/Grind/Propagate.lean
+++ b/src/Lean/Meta/Tactic/Grind/Propagate.lean
@@ -99,6 +99,8 @@ builtin_grind_propagator propagateNotUp ↑Not := fun e => do
   else if (← isEqTrue a) then
     -- a = True → (Not a) = False
     pushEqFalse e <| mkApp2 (mkConst ``Lean.Grind.not_eq_of_eq_true) a (← mkEqTrueProof a)
+  else if (← isEqv e a) then
+    closeGoal <| mkApp2 (mkConst ``Lean.Grind.false_of_not_eq_self) a (← mkEqProof e a)
 
 /--
 Propagates truth values downwards for a negation expression `Not a` based on the truth value of `Not a`.
diff --git a/tests/lean/run/grind_propagate_connectives.lean b/tests/lean/run/grind_propagate_connectives.lean
index e4f4a020dc68..6cb042ae1bba 100644
--- a/tests/lean/run/grind_propagate_connectives.lean
+++ b/tests/lean/run/grind_propagate_connectives.lean
@@ -103,3 +103,6 @@ example (p q r : Prop) : p ∨ (q ↔ r) → ¬r → q → False := by
   grind on_failure do
     Lean.logInfo "hello world"
     fallback
+
+example (a b : Nat) : (a = b) = (b = a) := by
+  grind