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