{A : Type} (P : A -> Type) {x y : A} {p1 p2 p3 : x = y} (r1 : p1 = p2) (r2 : p2 = p3) (z : P x) : transport2 P (r1 @ r2) z = transport2 P r1 z @ transport2 P r2 z. Proof. destruct r1, r2; reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.