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