>>859
>∀x.∃y.P(x,y)の証明が、λx.ex t f(x,t)の形をしてて、xがtに自由に現れないとき、ex t (λx.f(x,t))は∃y.∀x.P(x,t)の証明である。

ex t (λx.f(x,t))　が　∃y.∀x.P(x,t)　の証明であるとなぜ君の主張「∀が先頭についてるんだから相手側に全公開してるだろ」が正当化されるの？