{A : Type} (w x y z : list A) : app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z = ap (fun l => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z @ ap (fun l => l ++ z) (app_assoc w x y). Proof. symmetry. induction w as [|? w IHw] in x, y, z |- *. - simpl. apply equiv_p1_1q. lhs nrapply concat_p1. apply ap_idmap. - simpl. rhs_V nrapply ap_pp. rhs_V nrapply (ap (ap (cons a)) (IHw x y z)). rhs nrapply ap_pp. f_ap. { rhs nrapply ap_pp. f_ap. apply ap_compose. } lhs_V nrapply ap_compose. nrapply (ap_compose (fun l => l ++ z)). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum