Lemma prefix_remove_concatenate {A: decSet} (l1 l2 l3: list A) (tl: list A) : prefix_remove l1 l2 = ii1 tl → prefix_remove l1 (l2 ++ l3) = ii1 (tl ++ l3). Proof. revert l1 l2. refine (list_ind _ _ _). - intros l2 prooftl. apply ii1_injectivity in prooftl. rewrite prooftl. apply idpath. - intros x xs HPind. refine (list_ind _ _ _). + intro HP. cbv in HP. apply negpathsii2ii1 in HP. contradiction. + intros x2 x2s HP2. rewrite concatenateStep. induction (decproperty A x x2) as [xeqx2 | xneqx2]. * rewrite xeqx2. do 2 rewrite prefix_remove_stepeq. apply (HPind x2s). * rewrite (prefix_remove_stepneq xneqx2). intro HP. apply negpathsii2ii1 in HP. contradiction. Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.