Definition prefix_remove {A: decSet} (l1 l2: list A): maybe (list A). Proof. revert l1 l2. refine (list_ind _ _ _). - exact (λ l, just l). - intros x xs HP. refine (list_ind _ _ _). + exact nothing. + intros y ys _. induction (decproperty A x y). * exact (HP ys). * exact nothing. Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.