proposition: Lemma Vfilter_app : forall n (bs : bools n) n1 (v1 : vec n1) n2 (v2 : vec n2) (h : n=n1+n2), Vfilter (Vcast bs h) (Vapp v1 v2) = Vcast (Vapp (Vfilter (fst (Vbreak (Vcast bs h))) v1) (Vfilter (snd (Vbreak (Vcast bs h))) v2)) (Vtrue_break (Vcast bs h)).
proof: Proof. intros. apply Vfilter_app_eq. Qed.
imports: Coq(Arith) CoLoR(VecUtil LogicUtil EqUtil)