fact: Definition ap_pp {A B : Type} (f : A -> B) {x y z : A} (p : x = y) (q : y = z) : ap f (p @ q) = (ap f p) @ (ap f q) := match q with idpath => match p with idpath => 1 end end.
imports: Basics.Overture Basics.Tactics