Empty Context Misunderstanding
It says in the Standard that:
Note that, some proof rules
require an empty context. In the list of proof rules in Section 5 this is indicated by
omitting the Γ.
However, for a rule like:
It seems like the context should not be completely empty after applying the rule? What if we are inside of a subproof already (i.e., nested subproofs)?