proposition: Lemma Vopt_filter_cast p (xs : vector A p) p' (h : p = p') : forall n (ks : vector nat n), Vopt_filter ks (Vcast xs h) = Vopt_filter ks xs.
proof: Proof. subst p'. rewrite Vcast_refl. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)