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