Lemma prefix_remove_prefix {A: decSet} (l1 l2: list A): prefix_remove l1 (l1 ++ l2) = just l2. Proof. revert l1. refine (list_ind _ _ _). - reflexivity. - intros x xs IHl1. rewrite concatenateStep. rewrite prefix_remove_stepeq. assumption. Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.