Structural rules

structural rule Sequents as defined here are based on lists of formulas, so the rules for decomposing on the left must refer to the position of the formula. This is indicated by supplying a context around the formula, typically of the form $\bar{H}, x\!:\!F, \bar{J} \vdash G$. The cut cut rule rule specifies the exact location at which the formula is to be introduced into a hypothesis list, and thinthin does the same.

By combining applications of cut and thin, hypotheses can be moved (exchanged) or contracted. The so-called structural rulesstructural rule are included among these rules.