'simpl rewrite' can solve the problems in Factorization

Not the best solution, but better than what we had before.
Do you want to mention `Set Debug Unification` here as a way to discover things like this?