Lemma negpathsnilcons {A: UU} (a: A) (l: list A): [] != a :: l. Proof. intro X. apply pathsinv0 in X. apply negpathsconsnil in X. assumption. Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.