proposition: Lemma find_2 m x e : find x m = Some e -> MapsTo x e m.
proof: Proof. apply find_spec. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)