es5

Si tratta della proprieta' di subject reduction.
Infatti ci dice che in una sequenza di riduzioni
che parte da un termine ben tipato ogni termine rimarra' ben tipato e
del tipo del termine di partenza. Cosi', osservando che per ridurre un redex
("eseguire" una beta riduzione cioe' un passo di computazione) bisogna
tener conto solo della struttura del termine e non dei tipi,
ecco che, una volta controllato all'inizio che il termine e' ben tipato,
i tipi non concorrono piu' alla computazione.