Sequents

Once we have represented terms, it is quite an easy matter to represent a sequent $H \vdash G$. The goal G is a term and H is a list of terms. Actually, since some of the hypotheses are treated specially, we need to tag them with a boolean value, and hypotheses are labelled. So the actual definitions are these.

Definition

$$\times \times$$