{A : Type} (l l' : list A) : reverse (l ++ l') = reverse l' ++ reverse l. Proof. induction l as [|a l IHl] in l' |- *. 1: symmetry; apply app_nil. simpl. lhs nrapply reverse_cons. rhs nrapply ap. 2: nrapply reverse_cons. rhs nrapply app_assoc. nrapply (ap (fun l => l ++ [a])). exact (IHl l'). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum