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