GLのデネセシテーション
デネセシテーション
$ \vdash_\Lambda \Box A \implies \vdash_\Lambda A