slightly refine WPO-definition

• previous formalization of WPO deviated a bit to paper version (requiring less computation)
• both versions are equivalent whenever order in parameter is strongly normalizing
• however, this is no longer true for co-WPO, a variant of WPO with non strongly normalizing orders
• consequence: change formalization so that it is more closely related to paper version, so that also results on coWPO can be proven