proposition: Lemma Vfilter_break : forall n1 n2 (bs : bools (n1+n2)) (v : vec (n1+n2)), Vfilter bs v = Vcast (Vapp (Vfilter (fst (Vbreak bs)) (fst (Vbreak v))) (Vfilter (snd (Vbreak bs)) (snd (Vbreak v)))) (Vtrue_break bs).
proof: Proof. intros. apply Vfilter_break_eq. Qed.
imports: Coq(Arith) CoLoR(VecUtil LogicUtil EqUtil)