Lemma prefix_remove_stepback {A: decSet} (x1 x2: A) (xs1 xs2: list A) : prefix_remove (x1 :: xs1) (x2 :: xs2) != nothing → x1 = x2. Proof. induction (decproperty A x1 x2) as [x1eqx2 | x1neqx2] ; intro HP. - assumption. - rewrite (prefix_remove_stepneq x1neqx2) in HP. apply fromempty. apply (HP (idpath _)). Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.