{A : Type} (P : A -> Type) {x y z w : A} (p : x = y) (q : y = z) (r : z = w) (u : P x) : ap (fun e => e # u) (concat_p_pp p q r) @ (transport_pp P (p@q) r u) @ ap (transport P r) (transport_pp P p q u) = (transport_pp P p (q@r) u) @ (transport_pp P q r (p#u)) :> ((p @ (q @ r)) # u = r # q # p # u) . Proof. destruct p, q, r. simpl. exact 1. Defined.
Require Import Basics.Overture Basics.Tactics.