proposition: Lemma Vfilter_cons_eq : forall n (bs : bools (S n)) x (v : vec n) (h' : Vtrue_cons bs = Vtrue bs), 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) h'.
proof: Proof. intros n bs. VSntac bs. unfold Vtrue_cons. case (Vhead bs); simpl; intros. rewrite Vcast_refl. refl. rewrite Vcast_refl. refl. Qed.
imports: Coq(Arith) CoLoR(VecUtil LogicUtil EqUtil)