proposition: Lemma elements_mapsto : forall (s:t elt) x e, InA eqke (x,e) (elements s) <-> MapsTo x e s.
proof: Proof. intros; generalize (elements_aux_mapsto s nil x e); intuition. inversion_clear H0. Qed.
imports: FunInd FMapInterface FMapList ZArith Int