proposition: Lemma FindWithDefault_dec : forall {A : Type} (key : TKey) (default : A) (fmap : t A), { exists result, MapsTo key result fmap /\ @FindWithDefault A key default fmap = result } + { find key fmap = None /\ @FindWithDefault A key default fmap = default }.
proof: Proof. unfold FindWithDefault; intros A key default fmap; destruct (find key fmap) eqn:find; [ left; rewrite <- find_mapsto_iff in find | right ]; 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