Considerate le cinque famiglie di alberi che si ottengono 'valutando'
un lambda termine (alberi di Berarducci, di Bohm, di Lévy-Longo, eta-
alberi ed infiniti eta-alberi), si introduce un sistema di
assegnamento di tipo che è parametrico rispetto a queste famiglie. 

Successivamente si dimostra, in modo (quasi) uniforme, che ognuno di
questi sistemi di assegnamento di tipo descrive completamente
l'equivalenza osservazionale indotta dalla corrispondente
rappresentazione ad albero dei lambda termini. Più precisamente, per
ogni famiglia di alberi, due lambda-termini hanno lo stesso albero se,
e solo se, ad essi si possono assegnare gli stessi tipi nel
corrispondente sistema di assegnamento di tipo.