fact: Definition lift_relation_gen_hetero {A B P} (and : P -> P -> P) (True : P) (R : A -> B -> P) (defaultA : A) (defaultB : B) : t A -> t B -> P := fun m1 m2 => fold (fun _ => and) (map2 (fun x1 x2 => match x1, x2 with | Some x1, Some x2 => Some (R x1 x2) | Some x, None => Some (R x defaultB) | None, Some x => Some (R defaultA x) | None, None => None end) m1 m2) True.
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