fact: Definition lexv {n A} (eq gt : relation A) : relation (vector A n) := fun v w => lexn eq gt (prod_of_vec v) (prod_of_vec w).
imports: Coq(Morphisms Basics) CoLoR(SN LogicUtil NatUtil VecUtil VecOrd ListUtil RelUtil)