生成補題と型の一意性

(1) $\Gamma\vdash x:A$ ならば $(x{:}A)\in\Gamma$。$\Gamma\vdash\lambda x{:}A.M:C$ ならば、ある $B$ について $C\equiv A\to B$ かつ $\Gamma,x{:}A\vdash M:B$。$\Gamma\vdash MN:B$ ならば、ある $A$ について $\Gamma\vdash M:A\to B$ かつ $\Gamma\vdash N:A$。

(2) $\Gamma\vdash M:A$ かつ $\Gamma\vdash M:A'$ ならば $A\equiv A'$。また、$\Gamma\vdash M:A$ の導出はただ一つである。