fact: Definition transport_transport {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).
imports: Basics.Overture Basics.Tactics