diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 8c425b3c8f..46fa8095e3 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -113,7 +113,7 @@ macro_rules | `($x > $y)  => `(binrel% GT.gt $x $y)
 macro_rules | `($x >= $y) => `(binrel% GE.ge $x $y)
 macro_rules | `($x ≥ $y)  => `(binrel% GE.ge $x $y)
 macro_rules | `($x = $y)  => `(binrel% Eq $x $y)
-macro_rules | `($x == $y) => `(binrel% BEq.beq $x $y)
+macro_rules | `($x == $y) => `(binrel_no_prop% BEq.beq $x $y)
 
 infixr:35 " /\\ " => And
 infixr:35 " ∧ "   => And
diff --git a/tests/lean/run/764.lean b/tests/lean/run/764.lean
new file mode 100644
index 0000000000..6f4d0c5162
--- /dev/null
+++ b/tests/lean/run/764.lean
@@ -0,0 +1,6 @@
+#eval (5 > 2) == true
+#eval (2 > 5) == true
+
+variable (b : Bool)
+
+#check (5 > 2) == b