Definition disassembleSequence {X} : Sequence X -> coprod unit (X × Sequence X). Proof. intros x. induction x as [n x]. induction n as [|n]. - exact (ii1 tt). - exact (ii2(x lastelement,,(n,,x ∘ dni_lastelement))). Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.