proposition: Lemma Vfilter_break_eq : forall n1 n2 (bs : bools (n1+n2)) (v : vec (n1+n2)) (h : Vtrue (fst (Vbreak bs)) + Vtrue (snd (Vbreak bs)) = Vtrue bs), Vfilter bs v = Vcast (Vapp (Vfilter (fst (Vbreak bs)) (fst (Vbreak v))) (Vfilter (snd (Vbreak bs)) (snd (Vbreak v)))) h.
proof: Proof. induction n1; simpl. intros. rewrite Vcast_refl. refl. intros n2 bs v. VSntac bs. VSntac v. simpl. case (Vhead bs); simpl; intros. rewrite Vcast_cons. f_equal. apply IHn1. apply IHn1. Qed.
imports: Coq(Arith) CoLoR(VecUtil LogicUtil EqUtil)