t_1t_2:T_{12}の箇所について

t_1t_2は関数適用そのもの

t_1t_2:T_{12}は関数適用t_1t_2をした結果の値の型がT_{12}になると言っている

型の部分のみに着目すると、Modus Ponensになっている