Avendo due lambda astrazioni,
il tipo del termine sara' necessariamente della forma

A -> B -> C

dove A e' il tipo del primo input e B quello del secondo.

A deve necessariamente essere un tipo freccia, poiche' l'input x
e' utilizzato in posizione funzionale.
Anche B deve essere un tipo freccia, poiche' l'input y e' utilizzato
in posizione funzionale.

Poiche' l'argomento di x e' (yx), il dominio del tipo di x
e il codominio del tipo di y debbono coincidere.
Inoltre, il tipo di x deve coincidere con il dominio del tipo di y,
mentre il codominio del tipo di x coincide necessariamente con C.

Poiche' questi vincoli debbono essere necessariamente soddisfatti
e non ce ne sono altri, il tipo piu' semplice che li soddisfa e' quello dato.

Questi sono esattamente i vincoli che si ottengono se cerchiamo
di ricostruire una derivazione per il termine dato.