{A B} (P : A -> B -> Type) {x1 x2 : A} {y1 y2 : B} (p : x1 = x2) (q : y1 = y2) (z : P x1 y1) : P x2 y2 := transport (fun x => P x y2) p (transport (fun y => P x1 y) q z).
Require Import Basics.Overture Basics.Tactics.