Brevemente,

Perche' il tipo fornito e' una sostituzione del tipo principale 
del termine, che e' a->(a->b)->c

Enunciare il lemma di sostituzione 
e dimostrare, anche intuitivamente che 
a->(a->b)->c e il tipo principale del termine