{A B} (f:A->B) {x y z:A} {p p':x=y} {q q':y=z} (r:p=p') (s:q=q') : ap02 f (r @@ s) = ap_pp f p q @ (ap02 f r @@ ap02 f s) @ (ap_pp f p' q')^. Proof. case r, s, p, q. reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.