proposition: Lemma FindWithDefault_MapsTo : forall {A} default key (value: A) tree, MapsTo key value tree -> FindWithDefault key default tree = value.
proof: Proof. unfold FindWithDefault; intros ? ? ? ? ? maps_to. rewrite find_mapsto_iff in *. rewrite maps_to; 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