proposition: Lemma in_elements_mapsto : forall {A: Type} k (e: A) (m: t A), List.In (k, e) (elements m) -> MapsTo k e m.
proof: Proof. intros; eauto using elements_2, In_InA, equiv_eq_key_elt. Qed.
imports: Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Program.Program Coq.Structures.OrderedTypeEx Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances