seq_succ@{} (n : nat) : seq n.+1 = seq n ++ [n]. Proof. apply reverse_cons. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum