Manipulating Expressions
E — expression, u — expression variable
box E — term, x — term variable
let box u = M in N —
substitute expression denoted by M for u in N
embed(x) = let box u = x in box (...u...)
eval(x) = let box u = x in u
simplify(x) = case x of box (0*u) Þ box (0) | ...