Lemma isprefix_self {A: decSet} (l: list A): isprefix l l. Proof. unfold isprefix. rewrite prefix_remove_self. apply negpathsii1ii2. Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.