fact: Fixpoint vec_opt_of_list A m (l : list A) : vector (option A) m := match m with | 0 => Vnil | S m' => match l with | nil => Vconst None (S m') | cons x l' => Vcons (Some x) (vec_opt_of_list m' l') end end.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)