Offer multiple reduction choices per subterm, if applicable

[brprice]

There are cases where we could say that the same subterm could reduce in two different ways. E.g. let x = y in case C ... of C y -> x + y, where we could either reduce the case-of-known-constructor to let x = y in let y = ... in x + y, or rename the binders of the case branch so that we could then inline the let via let x = y in case C ... of C z -> let y = z in x + y. Since EvalFull is the "primary" evaluation method, we want to do the second (as it will, in a few steps, enable us to remove the outer let). However, we possibly want to make a different choice (or offer both) for the interactive evaluator.

However, it is not entirely clear whether this will still be an issue when/if we switch to explicit-substitution style pushing-down-lets, #44 . We should revisit it at that point.

Originally posted by @brprice in #718 (comment)

[dhess]

I've marked this as high priority not necessarily because it is actually high priority, but just so that we don't lose track of it once #736 is implemented.