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