proposition: Lemma in_elements_after_map : forall {A B: Type} (proc: A -> B) (m: t A) (x: B), List.In x (List.map snd (elements (map proc m))) -> exists k pred, MapsTo k pred m /\ proc pred = x.
proof: Proof. intros ? ? ? ? ? in_map; rewrite in_map_iff in in_map; destruct in_map as [(k, e) (is_proc, in_elements)]; apply in_elements_mapsto in in_elements; rewrite map_mapsto_iff in in_elements; destruct in_elements as [e_pred (is_pred, maps_to)]; exists k; exists e_pred; subst; intuition. 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