I want to disagree, but honestly the recursive method I tend to use is almost isomorphic to a loop + stack/deque. Eager elimination of `x=t` pairs, or eager nor

I want to disagree, but honestly the recursive method I tend to use is almost isomorphic to a loop + stack/deque. Eager elimination of `x=t` pairs, or eager normalization of substitutions sounds potentially inefficient, imho it's better to check that on the fly upon selecting a pair.