Sequents

sequent The nodes of a proof tree are called sequents. They are a list of hypotheses separated by the assertion sign, $\vdash$ (called turnstile or proof sign) followed by the conclusion. A hypothesis can be a typing assumption such as $x\!:\!A$ for A a type or a labeled assertionlabeled assertion, such as $l\!:\!P(x)$. The label lis used to refer to the hypothesis in the rules. The occurrence of x in $x\!:\!A$ is an individual variable, and we are assuming that it is an object of type A. So it is an assumption that A is inhabitedinhabited. Here is a sequent,

      $x_1:H_1, \ldots, x_n: H_n \vdash G$     

where H_i is an assertion or a type and x_i is either a label or a variable respectively. The x_i are all distinct. G is always an unlabeled formula. We can also refer to the hypothesis by number, $1 \ldots n$, and we refer to G as the 0-th component of the sequent. We abbreviate a sequent by $\bar{H} \vdash G$ for $\bar{H} = \left(x_1 : H_1, \ldots, x_n: H_n\right)$; sometimes we write $\bar{x}: \bar{H} \vdash G$.