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