proposition: Lemma min_elt_MapsTo m x e : min_elt m = Some (x,e) -> MapsTo x e m.
proof: Proof. intros. unfold min_elt in *. rewrite bindings_mapsto_iff. destruct (bindings m). simpl; try discriminate. destruct p; simpl in *. injection H; intros; subst; constructor; compute; auto with *. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)