proposition: Lemma Vfilter_cast_eq : forall n (bs : bools n) p (v : vec p) (hpn : p=n) (hnp: n=p) (h' : Vtrue (Vcast bs hnp) = Vtrue bs), Vfilter bs (Vcast v hpn) = Vcast (Vfilter (Vcast bs hnp) v) h'.
proof: Proof. induction bs; induction p; simpl; intros; try discr; revert h'; [rewrite Vcast_refl | rewrite Vcast_cons]; intros. rewrite Vcast_refl; refl. VSntac v. simpl. generalize h'. clear h'. case h; simpl; intro; rewrite Vcast_cons; simpl. rewrite Vcast_cons; f_equal; apply IHbs. apply IHbs. Qed.
imports: Coq(Arith) CoLoR(VecUtil LogicUtil EqUtil)