This might be a bit of a dumb question, but after pondering for a while I can't arrive to a conclusion which satisfies me.
In minimal logic, the elimination rule for $\forall$ is as follows:
$\forall x . A$
___________.
$A[x/t]$
While the introduction rule for implication is
$[A]$
$\vdots$
$B$
_______.
$A \implies B$
Given this information, my deduction for $(\forall x . P) \implies P$ would be the following:
$[\forall x . P]$
______________.
$P[x/t] \equiv P$
___________________.
$(\forall x . P) \implies P$
But what bothers me is that the conclusion $P$ seems to depend on an implicit assumption that $P$ was previously known to be deducible but that is not reflected anywhere in the proof tree nor the deduction rules for Natural deduction in minimal logic. How can this be then?
Also, considering that I'm studying this because I'm interested in constructive mathematics, what does this tell us about the mystery term $t$? Where do we get it from if everything is supposed to be constructed?