proposition: Lemma Vfilter_cast : forall n (bs : bools n) p (v : vec p) (h : p=n), Vfilter bs (Vcast v h) = Vcast (Vfilter (Vcast bs (sym_eq h)) v) (Vtrue_cast bs (sym_eq h)).
proof: Proof. intros. apply Vfilter_cast_eq. Qed.
imports: Coq(Arith) CoLoR(VecUtil LogicUtil EqUtil)