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