{A : Type} (Q : A -> Type) {x y : A} {p q : x = y} (r : p = q) (z : Q x) : transport2 Q r z = ap10 (ap (transport Q) r) z := match r with idpath => 1 end.
Require Import Basics.Overture Basics.Tactics.