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