proposition: Lemma Vfilter_app_eq : forall n (bs : bools n) n1 (v1 : vec n1) n2 (v2 : vec n2) (h : n=n1+n2) (h' : Vtrue (fst (Vbreak (Vcast bs h))) + Vtrue (snd (Vbreak (Vcast bs h))) = Vtrue (Vcast bs h)), Vfilter (Vcast bs h) (Vapp v1 v2) = Vcast (Vapp (Vfilter (fst (Vbreak (Vcast bs h))) v1) (Vfilter (snd (Vbreak (Vcast bs h))) v2)) h'.
proof: Proof. induction bs; intros. destruct n1; destruct n2; repeat rewrite Vcast_refl; solve [discr | refl]. destruct n1; try VOtac; repeat rewrite Vcast_refl; try solve [discr | refl]. revert h'; rewrite (Vcast_cons h0); simpl; intro h'. VSntac v1. destruct h; simpl; try apply IHbs. rewrite Vcast_cons; f_equal; apply IHbs. Qed.
imports: Coq(Arith) CoLoR(VecUtil LogicUtil EqUtil)