proposition: Lemma MapsTo_snd : forall {A: Type} val tree, (exists key, MapsTo key val tree) <-> List.In val (List.map snd (elements (elt:=A) tree)).
proof: Proof. split; intro H; [ destruct H as [key mapsto]; apply (InA_In_snd key); apply elements_1 | rewrite in_map_iff in H; destruct H as [(key, val') (eq_val_val', in_lst)]; subst; simpl; exists key; apply in_elements_mapsto ]; trivial. 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