diff --git a/src/Init/Grind/Lemmas.lean b/src/Init/Grind/Lemmas.lean
index 2c455598db87..180e63755f94 100644
--- a/src/Init/Grind/Lemmas.lean
+++ b/src/Init/Grind/Lemmas.lean
@@ -7,6 +7,7 @@ prelude
 import Init.Core
 import Init.SimpLemmas
 import Init.Classical
+import Init.ByCases
 
 namespace Lean.Grind
 
@@ -41,6 +42,9 @@ theorem not_eq_of_eq_false {a : Prop} (h : a = False) : (Not a) = True := by sim
 theorem eq_false_of_not_eq_true {a : Prop} (h : (Not a) = True) : a = False := by simp_all
 theorem eq_true_of_not_eq_false {a : Prop} (h : (Not a) = False) : a = True := by simp_all
 
+theorem true_eq_false_of_not_eq_self {a : Prop} (h : (Not a) = a) : True = False := by
+  by_cases a <;> simp_all
+
 /-! Eq -/
 
 theorem eq_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a = b) = b := by simp [h]
diff --git a/src/Lean/Meta/Tactic/Grind/Propagate.lean b/src/Lean/Meta/Tactic/Grind/Propagate.lean
index 6a41c0ab44e6..d3f038a25336 100644
--- a/src/Lean/Meta/Tactic/Grind/Propagate.lean
+++ b/src/Lean/Meta/Tactic/Grind/Propagate.lean
@@ -105,12 +105,13 @@ This function performs the following:
 - If `(Not a) = True`, propagates `a = False`.
 -/
 builtin_grind_propagator propagateNotDown ↓Not := fun e => do
+  let_expr Not a := e | return ()
   if (← isEqFalse e) then
-    let_expr Not a := e | return ()
     pushEqTrue a <| mkApp2 (mkConst ``Lean.Grind.eq_true_of_not_eq_false) a (← mkEqFalseProof e)
   else if (← isEqTrue e) then
-    let_expr Not a := e | return ()
     pushEqFalse a <| mkApp2 (mkConst ``Lean.Grind.eq_false_of_not_eq_true) a (← mkEqTrueProof e)
+  else if (← isEqv e a) then
+    pushEqFalse (← getTrueExpr) <| mkApp2 (mkConst ``Lean.Grind.true_eq_false_of_not_eq_self) a (← mkEqProof e a)
 
 /-- Propagates `Eq` upwards -/
 builtin_grind_propagator propagateEqUp ↑Eq := fun e => do
diff --git a/tests/lean/run/grind_pre.lean b/tests/lean/run/grind_pre.lean
index 1c28798093eb..551446308b46 100644
--- a/tests/lean/run/grind_pre.lean
+++ b/tests/lean/run/grind_pre.lean
@@ -124,3 +124,6 @@ example (a : α) (p q r : Prop) : (h₁ : HEq p a) → (h₂ : HEq q a) → (h
 
 example (a b : Nat) (f : Nat → Nat) : (h₁ : a = b) → (h₂ : f a ≠ f b) → False := by
   grind
+
+example (a : α) (p q r : Prop) : (h₁ : HEq p a) → (h₂ : HEq q a) → (h₃ : p = r) → q = r := by
+  grind