proposition: Lemma prefix_remove_stepneq {A: decSet} {x1 x2: A} (p: x1 != x2) (xs1 xs2: list A) : prefix_remove (x1 :: xs1) (x2 :: xs2) = nothing.
proof: Proof. unfold prefix_remove. cbn. induction (decproperty A x1 x2). - contradicts a p. - apply idpath. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.Combinatorics.Vectors UniMath.Combinatorics.Lists UniMath.Combinatorics.DecSet UniMath.Combinatorics.Maybe