proposition: Lemma elements_1 : forall m x e, MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
proof: Proof. intros; unfold elements, MapsTo, eq_key_elt; rewrite elements_mapsto; auto. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia