{A B} (C : A -> B -> Type) {x1 x2 : A} (p : x1 = x2) {y1 y2 : B} (q : y1 = y2) (c : C x1 y1) : transport (C x2) q (transport (fun x => C x y1) p c) = transport (fun x => C x y2) p (transport (C x1) q c). Proof. destruct p, q; reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.