{A B : Type} {C : B -> Type} {x y : A} (p : x = y) (M : forall a b, C b) : ap (fun a b => M a b) p = path_forall _ _ (fun b => ap (fun a => M a b) p). Proof. destruct p; symmetry; simpl; apply path_forall_1. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids