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