squash lib/monads: add symmetric bipred_disj_op_eq

Signed-off-by: Corey Lewis <[email protected]>
seL4 · Aug 31, 2023 · 1532ec6 · 1532ec6
1 parent 41c4adf
commit 1532ec6
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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