Lemma length_zero_back {A: UU} (l: list A): length l = 0 → l = []. Proof. revert l. refine (list_ind _ _ _). - reflexivity. - intros x xs _ HP. apply negpathssx0 in HP. contradiction. Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.