fact: Definition opt_pred(A B : Type)(P : A -> B -> Prop)(opt_a : option A)(opt_b : option B) := match opt_a with | Some a => match opt_b with | Some b => P a b | None => False end | None => match opt_b with | Some _ => False | None => True end end.
imports: FCF.FCF