We reify to a representation of expressions that includes an explicit
constructor for closed terms. Substitution can then be implemented as
the identify, which enables us to perform it using computation.