{A B C : Type} {x y : A} (p : x = y) (M : A -> B -> C) (N : A -> B) : ap (fun a => (M a) (N a)) p = ap11 (ap M p) (ap N p) := match p with 1 => 1 end.
Require Import Basics.Overture Basics.PathGroupoids Basics.Decidable Require Import Types.Forall.