proposition: Lemma isprefix_self {A: decSet} (l: list A): isprefix l l.
proof: Proof. unfold isprefix. rewrite prefix_remove_self. apply negpathsii1ii2. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.Combinatorics.Vectors UniMath.Combinatorics.Lists UniMath.Combinatorics.DecSet UniMath.Combinatorics.Maybe