proposition: Lemma Vin_filter_intro : forall A n (l : list (N n)) (v : vector A n) i (hi : i<n), In (N_ hi) l -> Vin (Vnth v hi) (Vfilter l v).
proof: Proof. induction l; simpl; intros. hyp. destruct a. destruct H. left. apply Vnth_eq. inversion H. subst. refl. right. apply IHl. hyp. Qed.
imports: CoLoR(VecUtil ListUtil NatUtil LogicUtil ListNodup BoundNat)