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.