Notation for Yichen's paper

Figure 4 in Yichen's paper uses some notation that might not be familiar. Here are some notes to help you along:

• The turnstile symbol ⊢, in "G ⊢ x", basically means "x is true in the environment G".
• The horizontal line is called a "rule": if all the things above the line are true, then the thing below the line must be true.

The Wikipedia page on sequents has more details.