seq_rev_seq_rev'@{} (n : nat) : list_map pr1 (seq_rev' n) = seq_rev n. Proof. induction n as [|n IHn]. 1: reflexivity. simpl; f_ap. lhs_V nrapply list_map_compose. apply IHn. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum