proposition: Lemma Vfilter_in : forall n bs (v : vec n) x, Vin x (Vfilter bs v) -> Vin x v.
proof: Proof. induction v. VOtac. simpl. auto. VSntac bs. simpl. case (Vhead bs); simpl; intros. decomp H0. subst x. auto. right. eapply IHv. apply H1. right. eapply IHv. apply H0. Qed.
imports: Coq(Arith) CoLoR(VecUtil LogicUtil EqUtil)