Does Kannan's theorem imply that NEXPTIME^NP ⊄ P/poly? I was reading a paper of Buhrman and Homer “Superpolynomial Circuits, Almost Sparse Oracles and the Exponential Hierarchy”.

On the bottom of page 2 they remark that the results of Kannan imply that $NEXPTIME^{NP}$ does not have polynomial size circuits. I know that in the exponential time hierarchy, $NEXPTIME^{NP}$ is just $\Sigma_2EXP$, and I also know that Kannan's result is that $\forall c\mbox{   }\exists L\in\Sigma_2P$ such that $L \not\in Size(n^c)$. Of course, Kannan's theorem is NOT saying $\Sigma_2P \not\subset P/poly$ (in order for that to be the case we would need to show that $\exists L\in\Sigma_2P$ such that $\forall c$, $L \not\in Size(n^c)$. However, I don't see how Kannan's result implies that $NEXPTIME^{NP} \not\subset P/poly$?
This version of the answer incorporates feedback from Emil Jeřábek.
As far as I can see, the main twist is that there is a language in $\mathsf{EXP}^{\Sigma^\mathsf{P}_2}$ of exponential circuit complexity. In particular, fix a binary encoding of boolean circuits and define $L$ as the language defined by

$L_n$ is not decided by any circuit of size $2^{n/2}$, and
any language $L'_n \subseteq \{0,1\}^n$ which precedes $L_n$ lexicographically is decided by some circuit $C$ of size at most $2^{n/2}$,

where the notation $L_n$ means the slice $L_n = L \cap \{0,1\}^n$.
To do this in exponential time with a $\Sigma_2^\mathsf{P}$ oracle, you can use binary search over subsets of $\{0,1\}^n$ (think of them as $2^n$ bit integers) to find the first such set which has circuit complexity $&gt; 2^{n/2}$. You just keep the current guess of $L_n$, and use the oracle to test if there exists a $L'_n \prec_{\text{lex}} L_n$ of circuit complexity at least $2^{n/2}$. Since this gives a machine in $\mathsf{EXP}^{\Sigma^\mathsf{P}_2}$ which writes down the whole slice $L_n$, clearly we can also decide membership in $L_n$, and, therefore, in $L$.
This is very much as in Kannan's argument, but scaled up and streamlined to use the exponential time. Then you should be able to use a scaled-up version of the Karp-Lipton theorem to show that if $\mathsf{NEXP} \subseteq \mathsf{P/poly}$, then $\mathsf{EXP}^{\Sigma^\mathsf{P}_2} \subseteq \mathsf{NEXP}^{\mathsf{NP}}$, and you can carry out the case analysis in Kannan's proof.