{A : Type} (B C : A -> Type) (D : forall a:A, B a -> C a -> Type) {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D x1 y z) : D x2 (p # y) (p # z) := match p with idpath => w end.
Require Import Basics.Overture Basics.Tactics.