I'm looking for a reference for complete problems for $FNP^{NP}$, i.e., the class of functional problems solvable by a polynomial time non-deterministic Turing machine that has access to an $NP$-oracle. For example, I'm pretty sure that the following problem $$R_{\exists\forall} := \{(\psi(x,y), u) \mid u \in \{0,1\}^{|x|} \ \text{and} \ \forall v \in \{0,1\}^{|y|} : \psi(u,v) = 1 \},$$ where $\psi(x,y)$ is a boolean formula (here $x$ and $y$ are tuples of boolean variables), is such a problem, but I'm unable to find a reference for this (or, in fact, for any other problem). To clarify, $R_{\exists\forall}$ is expressing the following functional problem: given $\psi(x,y)$, find $u \in \{0,1\}^{|x|}$ such that for every $v \in \{0,1\}^{|y|}$ we have that $\psi(u,v) = 1$. I don't think it is particularly difficult to show that $R_{\exists\forall}$ is $FNP^{NP}$-complete, but I would prefer to use a reference.
EDIT: I'm now wondering whether anybody has even defined $FNP^{NP}$ formally in the literature. Would also be interested in any reference where this is done.
