proposition: Lemma Vopt_filter_map : forall p (xs : vector A p) n (ks : vector nat n), Vopt_filter ks (Vmap f xs) = Vmap fopt (Vopt_filter ks xs).
proof: Proof. intros p xs. induction ks as [|k ks]; simpl. refl. rewrite IHks. destruct (lt_dec k p). rewrite Vnth_map. refl. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)