seq'@{} (n : nat) : list {k : nat & (k < n)%nat} := reverse (seq_rev' n).
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum