proposition: Lemma elements_1 : forall m x e, MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
proof: Proof. intros m; apply Raw.elements_1. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses