fact: Fixpoint vec_of_list (l : list A) : vector A (length l) := match l with | nil => Vnil | cons x m => Vcons x (vec_of_list m) end.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)