proposition: Lemma Vfilter_cons : forall n (bs : bools (S n)) x (v : vec n), Vfilter bs (Vcons x v) = Vcast ( if Vhead bs as b return vec (Vtrue_cons_if b bs) then Vcons x (Vfilter (Vtail bs) v) else Vfilter (Vtail bs) v) (Vtrue_cons_eq bs).
proof: Proof. intros. apply Vfilter_cons_eq. Qed.
imports: Coq(Arith) CoLoR(VecUtil LogicUtil EqUtil)