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