proposition: Lemma find_default_map2_defaulted {elt elt' elt''} (f : elt -> elt' -> elt'') default default' default'' (Hdefault'' : f default default' = default'') (m : t elt) (m' : t elt') k : find_default default'' k (map2 (defaulted_f default default' f) m m') = f (find_default default k m) (find_default default' k m').
proof: Proof. subst. erewrite find_default_map2 by reflexivity; reflexivity. 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