Definition assembleSequence {X} : coprod unit (X × Sequence X) -> Sequence X. Proof. intros co. induction co as [t|p]. - exact nil. - exact (append (pr2 p) (pr1 p)). Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.