squash lib/monads: add symmetric bipred_disj_op_eq

Signed-off-by: Corey Lewis <[email protected]>
seL4 · Aug 31, 2023 · 56bd415 · 56bd415
1 parent 41c4adf
commit 56bd415
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/lib/Monads/Fun_Pred_Syntax.thy b/lib/Monads/Fun_Pred_Syntax.thy
@@ -177,9 +177,8 @@ subsection "Simplification Rules for Lifted And/Or"
 
 lemma bipred_disj_op_eq[simp]:
   "reflp R \<Longrightarrow> ((=) or R) = R"
-  apply (rule ext, rule ext)
-  apply (auto simp: reflp_def)
-  done
+  "reflp R \<Longrightarrow> (R or (=)) = R"
+  by (auto simp: reflp_def)
 
 lemma bipred_le_true[simp]: "R \<le> \<top>\<top>"
   by clarsimp