{A B} (f : A -> B) (l : list A) : list_map f (reverse l) = reverse (list_map f l). Proof. nrapply list_map_reverse_acc. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum