proposition: Lemma Vmap_filter : forall (A B : Type) (f : A->B) n (bs : bools n) (v : vector A n), Vmap f (Vfilter bs v) = Vfilter bs (Vmap f v).
proof: Proof. induction v; intros; simpl. VOtac. refl. ded (IHv (Vtail bs)). VSntac bs. case (Vhead bs); simpl; rewrite H; refl. Qed.
imports: Coq(Arith) CoLoR(VecUtil LogicUtil EqUtil)