{A B : Type} (f : A -> B) {x y z : A} {w : B} (p : x = y) (q : y = z) (r : f z = w) : (ap f (p @ q)) @ r = (ap f p) @ (ap f q @ r). Proof. destruct p, q. simpl. exact (concat_pp_p 1 1 r). Defined.
Require Import Basics.Overture Basics.Tactics.