normal-order-reduce can β-reduce outermost expression
Reduce first function application argument if not lambda
Iterate for normal order reduction
Remove bogus β-reduce rule
Determine whether expression is reducible (and how)
β-reduction of a constant doesn't make sense
η-reduction of a constant makes no sense
Rename normal-order to old/normal-order
A better normal-order function
Refactor so normal-order produces a path
Rename step -> order
Refactor reduce
Simplify normal-order
Simplify normal-order