{A : Type} (l : list A) : reverse (reverse l) = l. Proof. induction l. 1: reflexivity. lhs nrapply ap. 1: nrapply reverse_cons. lhs nrapply reverse_app. exact (ap _ IHl). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum