Compare the order of this
Substitution with a given order.
The term order that is used for the resulting terms or formulas.
Substitution that is to be used underneath
Some kinds of substitutions can only be applied when pseudo-reduction is allowed to be performed.
Re-sort an object with a new