{A : Type} (a : A) (l : list A) : reverse (a :: l) = reverse l ++ [a]. Proof. induction l as [|b l IHl] in a |- *. 1: reflexivity. rewrite IHl. rewrite <- app_assoc. cbn; apply reverse_acc_cons. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum