fact: Definition defaulted_f {elt elt' elt''} (default : elt) (default' : elt') f := fun x y => match x, y return option elt'' with | Some x, Some y => Some (f x y) | Some x, None => Some (f x default') | None, Some y => Some (f default y) | None, None => None end.
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