{A : Type} (l l' : list A) : reverse_acc l' l = reverse l ++ l'. Proof. induction l as [|a l IHl] in l' |- *. 1: reflexivity. lhs nrapply IHl. lhs nrapply (app_assoc _ [a]). f_ap; symmetry. apply IHl. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum