proposition: Lemma prefix_remove_self {A: decSet} (l: list A): prefix_remove l l = just [].
proof: Proof. revert l. apply list_ind. - apply idpath. - intros x xs IH. rewrite prefix_remove_stepeq. apply IH. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.Combinatorics.Vectors UniMath.Combinatorics.Lists UniMath.Combinatorics.DecSet UniMath.Combinatorics.Maybe