とする.このとき が成立する. (証明の方針) ∀-除去 と置く.に対して 平行移動 である.そしてより と表示できる.推論中に仮定はないので,∀-導入可能.したがって ∀-導入 が成立する.
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。