Lemma prefix_remove_stepeq {A: decSet} (x: A) (xs1 xs2: list A) : prefix_remove (x :: xs1) (x :: xs2) = prefix_remove xs1 xs2. Proof. unfold prefix_remove. cbn. induction (decproperty A x x). - cbn. apply idpath. - contradiction (b (idpath x)). Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.