Nontrivial membership in NP Is there an example of a language which is in $NP$, but where we cannot prove this fact directly by showing that there exists a polynomial witness for membership in this language?

Instead, the fact that the language is in $NP$ would be proven by reducing it to another language in $NP$, where the link between the two is not trivial and needs careful analysis.

More generally, are there some interesting examples of problems in $NP$ so that it is hard to see that they are in $NP$? 

A semi-answer would be the problem of deciding the winner in parity games: to show that it is in $NP$ (even $NP\cap coNP$), we need the positional determinacy theorem which is deep and non-trivial. However this answer is not ideal, because it still boils down to the existence of a polynomial witness for this exact problem (the positional strategy), and does not reduce to another different $NP$-problem.

Another one would be the AKS primality algorithm: deciding whether a number is prime is polynomial, while there is a priori no small witness for this fact. Let's say we rule out the "surprising polynomial algorithms", since many of them would fit the description above. I'm more interested in surprising $NP$ algorithms which are not deterministic.
Integer Programming.

Showing that if there is an integer solution then there is a polynomial size integer solution is quite involved. See 


Christos Papadimitriou, "On the Complexity of Integer Programming", JACM, 1981.