型環境に含まれている変数で、型付けの際に消費されないようなものが存在していても良い

規則

\Gamma_1,\Gamma_2\vdash t:Tならば、

\Gamma_1,\;x:T_1,\;\Gamma_2\vdash t:Tとしてよい

補足

後者の型環境に冗長な型付けx:T_1が存在しても良い、というのがポイント

「x:T_1」があってもなくてもokということを言っている