seq_rev'@{} (n : nat) : list {k : nat & (k < n)%nat}. Proof. transparent assert (f : (forall n, {k : nat & (k < n)%nat} -> {k : nat & (k < n.+1)%nat})). { intros m. snrapply (functor_sigma idmap). intros k H. exact (leq_succ_r H). } induction n as [|n IHn]. 1: exact nil. nrefine ((n; _) :: list_map (f n) IHn). exact _. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum