∀x.∃y.P(x,y)の証明が、λx.ex t f(x,t)の形をしてて、xがtに自由に現れないとき、これこれが証明可能であるなんて、∃(x
÷1)野郎に分かるわけないじゃん