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