proposition: Lemma Vfilter_app : forall A n (l1 l2 : list (N n)) (v : vector A n), Vfilter (l1 ++ l2) v = Vcast (Vapp (Vfilter l1 v) (Vfilter l2 v)) (sym_eq (length_app l1 l2)).
proof: Proof. induction l1; simpl; intros. rewrite Vcast_refl. refl. rewrite Vcast_cons. f_equal. rewrite (IHl1 l2 v). apply Vcast_pi. Qed.
imports: CoLoR(VecUtil ListUtil NatUtil LogicUtil ListNodup BoundNat)