Some Error in Dag Prawitz 1970 Paper

It seems this paper is flawed:
SOME RESULTS FOR INTUITIONISTIC LOGIC WITH SECOND
ORDER QUANTIFICATION RULES
Dag Prawitz - 1970
https://www.sciencedirect.com/science/article/abs/pii/S0049237X08707572
The cut elimination might be valid.
But I guess he is jumping to conclusions
when he thinks that a proof:
|- ~ ∀x ~ A(x)
Has the existence property. The flaw
is easy to spot. He thinks that a proof,
with the non-invertible left hand ∀:
∀x B(x) |- C
Implies nevertheless a certain form of
invertibility in that there are terms
t1, .., tn such that we have a proof:
B(t1), ..., B(tn) |- C
Unless B is restricted to some special
set of formulas, I suspect that the above
is fallacious.
Any counter example that shows the fallacy?