proposition: Lemma Vfilter_cons_false : forall n b (bs : bools n) x (v : vec n) (h : b = false), Vfilter (Vcons b bs) (Vcons x v) = Vcast (Vfilter bs v) (Vtrue_cons_false bs h).
proof: Proof. intros. apply Vfilter_cons_false_eq. hyp. Qed.
imports: Coq(Arith) CoLoR(VecUtil LogicUtil EqUtil)