proposition: Lemma find_default_map2 {elt elt' elt''} f (H : f None None = None) default default' default'' (Hfl : forall v, f None (Some v) = f (Some default) (Some v)) (Hfr : forall v, f (Some v) None = f (Some v) (Some default')) (Hfd : f (Some default) (Some default') = Some default'') (m : t elt) (m' : t elt') k : find_default default'' k (map2 f m m') = option_rect (fun _ => elt'') (fun v => v) default'' (f (Some (find_default default k m)) (Some (find_default default' k m'))).
proof: Proof. unfold find_default. rewrite map2_1bis by assumption. do 2 edestruct find; simpl; rewrite ?Hfl, ?Hfr, ?Hfd, ?H; try 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