proposition: Lemma Vin_filter_elim_in : forall A n (l : list (N n)) (v : vector A n) x, Vin x (Vfilter l v) -> Vin x v.
proof: Proof. induction l; simpl; intros. contr. destruct H. subst. apply Vnth_in. apply IHl. hyp. Qed.
imports: CoLoR(VecUtil ListUtil NatUtil LogicUtil ListNodup BoundNat)