Fix coercion code to disallow using cumulativity in the domain of products, which
results in strange changes in user provided terms.
Use kernel conversion on terms that contain universe variables during unification, speeding it up considerably
Revert backwards-incompatible commit 77df7b1283940d979d3e14893d151bc544f41410