proposition: Lemma exists_spec : forall A f, Proper (X.eq ==> Logic.eq ==> Logic.eq) f -> forall dom (m : t A dom), exists_ f m = true <-> exists x v, find x m = Some v ∧ f x v = true.
proof: Proof. intros A f Hf dom m. unfold exists_, find. rewrite fold_spec. change (exists x (v : A), S.find x m = Some v ∧ f x v = true) with (exists x (v : A), S.find (fst (x, v)) m = Some (snd (x, v)) ∧ f x v = true). setoid_rewrite <- elements_spec. rewrite exists_spec_aux; intuition discriminate || eassumption. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface