Definition nil_length {X} (x : Sequence X) : length x = 0 <-> x = nil. Proof. intros. split. - intro e. induction x as [n x]. simpl in e. induction (!e). apply pathsinv0. apply nil_unique. - intro h. induction (!h). reflexivity. Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.