proposition: Corollary find_dom : forall A x v dom (m : t A dom), find x m = Some v -> Dom.In x dom.
proof: Proof. intros. rewrite <- find_spec. eexists; eassumption. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface