proposition: Lemma prefix_remove_concatenate2 {A: decSet} (l1 l2 l3: list A) : length l1 ≤ length l2 → prefix_remove l1 l2 = nothing → prefix_remove l1 (l2 ++ l3) = nothing.
proof: Proof. revert l1 l2. refine (list_ind _ _ _). - intros l2 Hlen Hpref. contradiction (negpathsii1ii2 _ _ Hpref). - intros x1 xs1 IH. refine (list_ind _ _ _). + intros Hlen Hpref. contradiction (negnatlehsn0 _ Hlen). + intros x2 xs2 _ Hlen Hpref. rewrite concatenateStep. induction (decproperty A x1 x2) as [x1eqx2 | x1neqx2]. * induction x1eqx2. rewrite prefix_remove_stepeq. rewrite prefix_remove_stepeq in Hpref. apply (IH xs2 Hlen Hpref). * apply (prefix_remove_stepneq x1neqx2). Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.Combinatorics.Vectors UniMath.Combinatorics.Lists UniMath.Combinatorics.DecSet UniMath.Combinatorics.Maybe