proposition: Lemma Vin_filter_elim_nth : forall A n (l : list (N n)) (v : vector A n) x, Vin x (Vfilter l v) -> exists i (hi : i<n), In (N_ hi) l /\ Vnth v hi = x.
proof: Proof. induction l; simpl; intros. contr. destruct a as [i hi]. destruct H. ex i hi. auto. destruct (IHl _ _ H) as [j h]. destruct h as [hj h]. ex j hj. intuition. Qed.
imports: CoLoR(VecUtil ListUtil NatUtil LogicUtil ListNodup BoundNat)