Theorem SequenceAssembly {X} : Sequence X ≃ unit ⨿ (X × Sequence X). Proof. intros. exists disassembleSequence. apply (isweq_iso _ assembleSequence). { intros. induction x as [n x]. induction n as [|n]. { apply nil_unique. } apply drop_and_append'. } intros co. induction co as [t|p]. { unfold disassembleSequence; simpl. apply maponpaths. apply proofirrelevancecontr. apply iscontrunit. } induction p as [x y]. induction y as [n y]. apply (maponpaths (@inr unit (X × Sequence X))). unfold append_vec, lastelement; simpl. unfold append_vec. simpl. induction (natlehchoice4 n n (natgthsnn n)) as [e|e]. { contradicts e (isirreflnatlth n). } simpl. apply maponpaths, maponpaths. apply funextfun; intro i. clear e. induction i as [i b]. unfold dni_lastelement; simpl. induction (natlehchoice4 i n (natlthtolths i n b)) as [d|d]. { simpl. apply maponpaths. now apply isinjstntonat. } simpl. induction d; contradicts b (isirreflnatlth i). Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.