Skip to content

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:

image

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)?

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information