関数適用の規則T-App
https://gyazo.com/64713bed2541b888107c4d2cb022f509
$ t_1t_2:T_{12}
の箇所について
$ t_1t_2
は関数適用そのもの
$ t_1t_2:T_{12}
は関数適用
$ t_1t_2
をした結果の値の型が
$ T_{12}
になると言っている
型の部分のみに着目すると、
Modus Ponens
になっている
https://gyazo.com/fbc29567b2c14ae5ad351e8aa9584f46