proposition: Lemma elements_mapsto_iff : forall m x e, MapsTo x e m <-> InA (@eq_key_elt _) (x,e) (elements m).
proof: Proof. split; [apply elements_1 | apply elements_2]. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface