Strengthen [sets] tactic

Frap.v

@@ -145,7 +145,33 @@ Ltac first_order := firstorder idtac.
 
 (** * Model checking *)
 
-Ltac sets := Sets.sets ltac:(simpl in *; intuition (subst; auto)).
+Lemma eq_iff : forall P Q,
+    P = Q
+    -> (P <-> Q).
+Proof.
+  equality.
+Qed.
+
+Ltac sets0 := Sets.sets ltac:(simpl in *; intuition (subst; auto; try equality; try linear_arithmetic)).
+
+Ltac sets := propositional;
+  try match goal with
+      | [ |- @eq (set _) _ _ ] =>
+        let x := fresh "x" in
+        apply sets_equal; intro x;
+        repeat match goal with
+               | [ H : @eq (set _) _ _ |- _ ] => apply (f_equal (fun f => f x)) in H;
+                                                apply eq_iff in H
+               end
+      end; sets0;
+  try match goal with
+      | [ H : @eq (set ?T) _ _, x : ?T |- _ ] =>
+        repeat match goal with
+               | [ H : @eq (set T) _ _ |- _ ] => apply (f_equal (fun f => f x)) in H;
+                                                 apply eq_iff in H
+               end;
+          solve [ sets0 ]
+      end.
 
 Ltac model_check_invert1 :=
   match goal with
@@ -252,3 +278,6 @@ Ltac simplify_map :=
     simplify_map' (m $+ (k, v)) tt ltac:(fun m' =>
                                            replace (@add A B m k v) with m' by maps_equal)
   end.
+
+Require Import Classical.
+Ltac excluded_middle P := destruct (classic P).