{A:Type} (B:A->Type) (C:sig B -> Type) (x1 x2:A) (p:x1=x2) (y:B x1) (z:C (x1;y)) : transportD B (fun a b => C (a;b)) p y z = transport C (path_sigma' B p 1) z. Proof. destruct p. reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.