proposition: Theorem find_None : forall A dom x (m : t A dom), find x m = None <-> ¬Dom.In x dom.
proof: Proof. intros. rewrite <- (find_spec x m). destruct (find x m). + split; intro Hfind. discriminate Hfind. elim Hfind. eexists; reflexivity. + split; intro Hfind. intros [? Habs]. discriminate Habs. reflexivity. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface