fact: Definition diag_None {A B C} (f : option A → option B → option C) (mx : option A) (my : option B) : option C := match mx, my with None, None => None | _, _ => f mx my end.
imports: Coq(Permutation) stdpp(options)