Notación: E(G) |- t:T significa que el término t está bien tipado y tiene tipo T en el entorno E y contexto G. WF(E) [G] significa que el entorno E está bien formado y que el contexto G es válido en este entorno.