Fix multi-step reductions

Split substitution in two: the α-conversions and the substitution itself (β-conversion). This way we can have the renamed term before the β conversion and have correct before/after terms on all steps.

Needs thorough testing :sweat_smile: