proposition: Lemma mem_spec : forall m x, mem x m = true <-> In x m.
proof: Proof. unfold In, MapsTo; intros m x; rewrite mem_find. split. - destruct (find x m). exists a; auto. intros; discriminate. - destruct 1 as (e0,H0); rewrite H0; auto. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)