proposition: Lemma Vfilter_app2 : forall n1 (bs1 : bools n1) (v1 : vec n1) n2 (bs2 : bools n2) (v2 : vec n2), Vfilter (Vapp bs1 bs2) (Vapp v1 v2) = Vcast (Vapp (Vfilter bs1 v1) (Vfilter bs2 v2)) (sym_eq (Vtrue_app bs1 bs2)).
proof: Proof. intros. apply Vfilter_app2_eq. Qed.
imports: Coq(Arith) CoLoR(VecUtil LogicUtil EqUtil)