{A B C : Type} {x y : A} (p : x = y) (M : A -> B -> C) : ap (fun a b => M a b) p = path_arrow _ _ (fun b => ap (fun a => M a b) p). Proof. destruct p; symmetry; simpl; apply path_arrow_1. Defined.
Require Import Basics.Overture Basics.PathGroupoids Basics.Decidable Require Import Types.Forall.