length_reverse_acc@{i|} {A : Type@{i}} (acc l : list A) : length (reverse_acc acc l) = (length acc + length l)%nat. Proof. symmetry. induction l as [|x l IHl] in acc |- * using list_ind@{i i}. - apply nat_add_zero_r. - rhs_V nrapply IHl. apply nat_add_succ_r. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum