Better substitution memoization

Currently, the substitution algorithm is memoized over its three input parameters: the original term, the term being substituted and the appropriate depth.

An interesting optimisation would be to consider a memoization over two parameters: the original term and the depth, while retaining the three-parameter memoization. This would of course not return a term, because it is not fully determined. Instead, it could return a skeleton, a sort of partial term indicating how to traverse the term to go perform the substitutions, ignoring the useless branches where no substitution occurs. This skeleton would be stored in the arena, along with its other dwellers.