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