* Bart jacobs, Categorical logic and type theory lists the followings as the basic rules of simple type theory: (1) *identity* $$\frac{}{x:X\vdash x:X}$$ (2) *function symbol* $$\frac{M_1:x_1\;\;\dots \;\; M_n:x_n}{F(M_1,\dots,M_n:x_{n+1}}$$ for $F:x_1,\dots,x_n\to x_{n+1}$ in $\Sigma$ (3) *weakening* (4) *contraction* (5) *exchange* where we omitted the $\Gamma \vdash$ which we could prefix to every typing judgement. From these rule one can derive a further important rule: (6) *substitution* $$\frac{x_n:s\vdash M:t\;\;\; N:s}{M[N/x_n]:t}$$