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