{A : Type} (x y z : list A) : app x (app y z) = app (app x y) z. Proof. induction x as [|a x IHx] in |- *. - reflexivity. - exact (ap (cons a) IHx). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum