# Reference for complete problems for $FNP^{NP}$

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.