proposition: Lemma exists_compat : forall x y, Equal x y -> exists_ f x = exists_ f y.
proof: Proof. intros x y H. apply <- bool_prop_iff. rewrite <- 2 exists_iff by apply Hcompat. unfold Exists. completer idtac; firstorder. Qed.
imports: Coq(FSets) ATBR(Common) ATBR(BoolView)