Lemma assembleSequence_ii2 {X} (p : X × Sequence X) : assembleSequence (ii2 p) = append (pr2 p) (pr1 p). Proof. reflexivity. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.