proposition: Lemma find_spec : forall A x dom (m : t A dom), (exists v, find x m = Some v) <-> Dom.In x dom.
proof: Proof. intros A x dom [m Hok]. unfold find. simpl. rewrite <- (Hok x). split; intros [v Hin]; exists v; apply S.find_1 || apply S.find_2; assumption. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface