proposition: Lemma Vfilter_head_false : forall n (bs : bools (S n)) x (v : vec n) (h : Vhead bs = false), Vfilter bs (Vcons x v) = Vcast (Vfilter (Vtail bs) v) (Vtrue_Sn_false bs h).
proof: Proof. intros. apply Vfilter_head_false_eq. hyp. Qed.
imports: Coq(Arith) CoLoR(VecUtil LogicUtil EqUtil)