fact: Definition concat_AT {A : Type} (P : A -> Type) {x y : A} {p q : x = y} {z w : P x} (r : p = q) (s : z = w) : ap (transport P p) s @ transport2 P r w = transport2 P r z @ ap (transport P q) s := match r with idpath => (concat_p1_1p _) end.
imports: Basics.Overture Basics.Tactics