Pro: letrec semantics would be bit cleaner, now we substitute in the complete letrec when evaluating a term-binding.
Pro: it would be consistent with an ADT implementation that uses environments (see #12 ), although the plan for now is to implement ADTS with substitution.
Subsitution-based
Pro: always reason about closed terms in other lemmas
Environment-based
Subsitution-based