{A B : Type} (f : A -> B) (l l' : list A) : list_map f (reverse_acc l' l) = reverse_acc (list_map f l') (list_map f l). Proof. revert l'; simple_list_induction l a l IHl; intro l'. 1: reflexivity. 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