* Bart jacobs, Categorical logic and type theory p.121-123 lists the following as the basic rules of simple type theory: (1) *identity* $$\frac{}{x:X\vdash x:X}$$ (2) *function symbol* $$\frac{M_1:s_1\;\;\dots \;\; M_n:s_n}{F(M_1,\dots,M_n:s_{n+1})}$$ for $F:s_1,\dots,s_n\to s_{n+1}$ in $\Sigma$ (3) *weakening* $$\frac{x_1:s_1,\;\dots\;x_n:s_n\vdash M:t}{x_1:s_1,\dots,x_n:s_n,x_{n+1},s_{n+1}\vdash M:t}$$ (4) *contraction* $$\frac{\Gamma, x_n: s, x_{n+1}: s\vdash M:t}{\Gamma, x_n: s\vdash M[x_n / x_{n+1}]: t}$$ (5) *exchange* $$\frac{\Gamma, x_i:s_i, x_{i+1}:s_{i+1},\Delta\vdash M: t}{\Gamma, x_i:s_{i+1}, x_{i+1}: s_i,\Delta\vdash M[x_i/x_{it1},x_{i+1}/x_i]:t}$$ where we omitted (except in (4) and (5)) 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}$$