Lower bounds for the size of nondeterministic circuits
A partial answer to the second question:


exponential lower bounds for explicit functions for any class that contains 3-CNF do not translate into exponential lower bounds for unlimited nondeterminism, because one can transform any circuit of size $S$ into a nondeterministic 3-CNF of size $O(S)$ with non-determinism $S$,
even if you want non-determinism less than S, this is still doable if the function is computed by a $B_2$ formula (for example, parity), because one can split this formula of size $S$ into, say, $S/100$ pieces introducing $S/100$ new variables, and the resulting formula will be $O(S)$ size (though the constant in the $O()$ will be large),
for limited (but growing) nondeterminism one can, of course, use good old bounds (for example, Hastad's exponential lower bound $2^{n^{1/d}}$ for parity remains exponential if the nondeterminism is much less than $n^{1/d}$: just enumerate all possible bits for the nondeterminism and take a big OR of the resulting formulas).


A partial answer to the first question:


not known to me :) it would be interesting to see the proof (in particular, how can you substitute values for the existential variables).