fact: Parameter combine_None : forall A B C (f : A -> B -> C) g₁ g₂ dom₁ dom₂ (m₁ : t A dom₁) (m₂ : t B dom₂) x, find x (combine f g₁ g₂ m₁ m₂) = None <-> find x m₁ = None ∧ find x m₂ = None.
imports: Utf8 Orders Coqlib DepMapInterface