proposition: Lemma prefix_remove_stepback {A: decSet} (x1 x2: A) (xs1 xs2: list A) : prefix_remove (x1 :: xs1) (x2 :: xs2) != nothing → x1 = x2.
proof: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.Combinatorics.Vectors UniMath.Combinatorics.Lists UniMath.Combinatorics.DecSet UniMath.Combinatorics.Maybe