proposition: Lemma Vfilter_app2_eq : forall n1 (bs1 : bools n1) (v1 : vec n1) n2 (bs2 : bools n2) (v2 : vec n2) (h : Vtrue bs1 + Vtrue bs2 = Vtrue (Vapp bs1 bs2)), Vfilter (Vapp bs1 bs2) (Vapp v1 v2) = Vcast (Vapp (Vfilter bs1 v1) (Vfilter bs2 v2)) h.
proof: Proof. induction bs1; simpl. intros. VOtac. simpl. rewrite Vcast_refl. refl. case h; simpl; intros; VSntac v1; simpl. rewrite Vcast_cons. f_equal. apply IHbs1. apply IHbs1. Qed.
imports: Coq(Arith) CoLoR(VecUtil LogicUtil EqUtil)