縮約規則
Contraction
同一の変数が複数回、型付けの際に現れても良い
これだけであまりはわからん、具体例を見たい #?? 規則
$ \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 としても良い
補足
記号が多いので、揃えて書くと
https://gyazo.com/e5341fa95cac874267777b16e11416d9
変数$ x_1が2回使われている
今回重要というわけでもないが「$ x_2\mapsto x_1 」はβ簡約