Lemma prefix_remove_drop {A: decSet} (l1 l2: list A) : prefix_remove l1 l2 != nothing → prefix_remove l1 l2 = just (drop l2 (length l1)). Proof. revert l1 l2. refine (list_ind _ _ _). - reflexivity. - intros x1 xs1 IH. refine (list_ind _ _ _). + contradiction. + intros x2 xs2 _ prefixok. induction (decproperty A x1 x2) as [x1eqx2 | x1neqx2]. * induction x1eqx2. rewrite prefix_remove_stepeq. rewrite prefix_remove_stepeq in prefixok. apply (IH xs2 prefixok). * rewrite (prefix_remove_stepneq x1neqx2) in prefixok. contradiction prefixok. apply idpath. Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.