diff --git a/lib/Monads/Fun_Pred_Syntax.thy b/lib/Monads/Fun_Pred_Syntax.thy
index 330034b136..2efacdc624 100644
--- a/lib/Monads/Fun_Pred_Syntax.thy
+++ b/lib/Monads/Fun_Pred_Syntax.thy
@@ -177,6 +177,7 @@ subsection "Simplification Rules for Lifted And/Or"
 
 lemma bipred_disj_op_eq[simp]:
   "reflp R \<Longrightarrow> ((=) or R) = R"
+  "reflp R \<Longrightarrow> (R or (=)) = R"
   apply (rule ext, rule ext)
   apply (auto simp: reflp_def)
   done