proposition: Lemma Vfilter_app_eq : forall A n (l l1 l2 : list (N n)) (v : vector A n) (e : length l1+length l2 = length l), l=l1++l2 -> Vfilter l v = Vcast (Vapp (Vfilter l1 v) (Vfilter l2 v)) e.
proof: Proof. intros. subst l. rewrite Vfilter_app. apply Vcast_pi. Qed.
imports: CoLoR(VecUtil ListUtil NatUtil LogicUtil ListNodup BoundNat)