The problem is taken out of Theory of Computational Complexity:
Now, I think I've successfully proven that $ALL_{NFA} = \{(A) : A$ is an NFA and $ L(A) = \Sigma^*\} \leq_p MIN_{NFA}$. Which implies that $MIN_{NFA}$ is PSPACE hard, as the latter is itself.
However I'm stuck proving this problem is in PSPACE - I've thought of defining a nondeterministic Turing Machine, that takes an NFA and a natural number $n$ as input, and on each branch of the computation creates a NFA with number of states less than or equal to $n$. This machine will go on to compare the resulting NFA (in each branch) to the given one (this problem is itself in PSPACE, but I've yet to prove it myself).
However it seems to me the above idea may use more than poly. time, as we may have to keep track of the transition function of each NFA; whose image is in the power set of its states.
Any assistance?