弱化規則
Weakening
型環境に含まれている変数で、型付けの際に消費されないようなものが存在していても良い
規則
$ \Gamma_1,\Gamma_2\vdash t:Tならば、
$ \Gamma_1,\;x:T_1,\;\Gamma_2\vdash t:Tとしてよい
補足
後者の型環境に冗長な型付け$ x:T_1が存在しても良い、というのがポイントmrsekut.icon
「$ x:T_1」があってもなくてもokということを言っている
https://en.wikipedia.org/wiki/Structural_rule
https://drive.google.com/file/d/1OxnETBYjtF7H9bRDtw5pmFpLzLC6lWjK/view