Drop empty context requirement
Currently many rules require an empty context. Those are the rules that existed prior to the 2017 work. The conclusion of those rules are often not equalities that fit the semantic of the context (t = u
).
However, it should be fine to drop this requirement and just say that the semantic for most rules is to ignore the context. This should be fine for two reasons (a) the rules that currently don't use a context only operate on closed terms where applying the context has no effect (b) the rules that "pop" off a binder to generated a term with free variables overwrite any prior substitution assigned to the now-free variable.
Removing the restriction requires a careful re-read of the specification document to see where we assume, or claim that something has an empty context. We should also mark rules that are not context aware.
See !2 (comment 70264) for a discussion of this change.