Definition prefix_remove_back {A: decSet} (l1 l2 l3: list A): prefix_remove l1 l2 = just l3 → l2 = l1 ++ l3. Proof. revert l1 l2. refine (list_ind _ _ _). - intros l2 prefixnil. cbn in prefixnil. apply just_injectivity in prefixnil. cbn. assumption. - intros x1 xs1 HPind. refine (list_ind _ _ _). + intro prefixxs. cbn in prefixxs. apply negpathsii2ii1 in prefixxs. contradiction. + intros x2 xs2 HP2ind HP. induction (decproperty A x1 x2) as [x1eqx2 | x1neqx2]. * rewrite x1eqx2 in *. rewrite prefix_remove_stepeq in HP. rewrite concatenateStep. rewrite (HPind xs2 HP). apply idpath. * rewrite (prefix_remove_stepneq x1neqx2) in HP. contradiction (negpathsii2ii1 _ _ HP). Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.