proposition: Lemma Vfilter_map : forall A B (f : A -> B) n (v : vector A n) (l : list (N n)), Vfilter l (Vmap f v) = Vmap f (Vfilter l v).
proof: Proof. induction l; simpl; intros. refl. rewrite IHl, Vnth_map. refl. Qed.
imports: CoLoR(VecUtil ListUtil NatUtil LogicUtil ListNodup BoundNat)