Move Params definition in generalize rewriting out of a section so that
its universe doesn't get constrained unnecessarily (bug found in MathClasse).
Also avoid using rewrite itself in a proof in Morphisms.
Really honor the [simpl never] flag in whd_simpl, it was still doing reductions in
case the constant was hiding a direct match for example. Also avoid two lookups
of ReductionBehavior per constant application in simpl.