proposition: Lemma Vfilter_cons_true_eq : forall n b (bs : bools n) x (v : vec n), b = true -> forall h : S (Vtrue bs) = Vtrue (Vcons b bs), Vfilter (Vcons b bs) (Vcons x v) = Vcast (Vcons x (Vfilter bs v)) h.
proof: Proof. intros n b bs x v H. subst b. simpl Vtrue. intro. rewrite Vcast_refl. refl. Qed.
imports: Coq(Arith) CoLoR(VecUtil LogicUtil EqUtil)