proposition: Lemma ap_transport_pV {X} (Y : X -> Type) {x1 x2 : X} (p : x1 = x2) {y1 y2 : Y x2} (q : y1 = y2) : ap (transport Y p) (ap (transport Y p^) q) = transport_pV Y p y1 @ q @ (transport_pV Y p y2)^.
proof: Proof. destruct p, q; reflexivity. Defined.
imports: Basics.Overture Basics.Tactics