proposition: Lemma Vfilter_cons_false_eq : forall n b (bs : bools n) x (v : vec n), b = false -> forall h : Vtrue bs = Vtrue (Vcons b bs), Vfilter (Vcons b bs) (Vcons x v) = Vcast (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)