proposition: Lemma In_MapsTo : forall A tree key, In key tree -> exists (value: A), (MapsTo key value tree /\ find key tree = Some value).
proof: Proof. intros A tree key H; apply in_find_iff in H; destruct (find key tree) as [value | ] eqn:eq_option; try rewrite <- find_mapsto_iff in eq_option; intuition eauto. 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