From 1532ec63b5233de366a38401fcaa1881d1c8b712 Mon Sep 17 00:00:00 2001
From: Corey Lewis <corey.lewis@proofcraft.systems>
Date: Thu, 31 Aug 2023 14:26:57 +1000
Subject: [PATCH] squash lib/monads: add symmetric bipred_disj_op_eq

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
---
 lib/Monads/Fun_Pred_Syntax.thy | 1 +
 1 file changed, 1 insertion(+)

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