fact: Fixpoint prod_of_vec n A (v : vector A n) := match v in vector _ n return prodn n A with | Vnil => tt | Vcons x v' => (x, prod_of_vec v') end.
imports: Coq(Morphisms Basics) CoLoR(SN LogicUtil NatUtil VecUtil VecOrd ListUtil RelUtil)