同一の変数が複数回、型付けの際に現れても良い

これだけであまりはわからん、具体例を見たい #??

規則

\Gamma_1,\;x_2:T_1,\;x_3:T_1,\;\Gamma_2\vdash t:T_2ならば、

\Gamma_1,\;x_1:T_1,\;\Gamma_2\vdash [x_2\mapsto x_1][x_3\mapsto x_1]t:T_2としても良い

補足

記号が多いので、揃えて書くと

変数x_1が2回使われている

今回重要というわけでもないが「x_2\mapsto x_1 」はβ簡約