Illusie told me last year that these tapes of his meetings with Grothendieck are somewhere in his basement where they're very hard to find, so they're certainly not online.
The recording of Illusie's reminisces of Grothendieck to which both posts link has been transcribed here. Drinfeld and Illusie will be releasing a more polished version at some point next year.
Set theory provides a good example. It is often convenient in set theory to work with the concept of "classes" and treat them as mathematical objects of their own kind. The standard axiomatization of set theory with classes is called Goedel-Bernays set theory, denoted GBC, whereas the usual ZFC axioms have only set objects. But there is a general theorem that any statement purely about sets that is proved by using classes in GBC can be proved without them purely in ZFC. This is what it means to say that GBC is a conservative extension of ZFC. To prove this general theorem, it suffices to observe that any ZFC model can be expanded to a model of GBC, by adding only the classes definable from parameters.
There are many other examples of conservative extensions in mathematics, and all of them would seem to be examples of the type that you seek. For example, PA has a conservative extension to the analogous theory true in the collection HF of hereditarily finite sets. Thus, to prove a theorem about numbers in PA, one can freely use heredtiarily finite sets (e.g. sequences of numbers, sequences of sets of numbers, etc.), not just as coded by numbers via Goedel coding, but as actual mathematical objects. And surely this makes proofs much easier.
Perhaps another type of example arises in the absoluteness phenomenon in set theory. For example, the Shoenfield Absoluteness theorem states that any Sigma^1_2 statement has the same truth value in any two models of set theory with the same ordinals. In particular, to prove that a particular Sigma^1_2 statement is true in ZFC, it suffices to prove it under the assumption also that V=L, where one also has all kinds of additional structure available. The Absoluteness Theorems (and there are many) can therefore be viewed under the rubric you mention.
But of course, in all these cases, we have an actual proof in the weaker theory. To prove that there is a proof, is a proof, so I believe ultimately there will be no way to avoid the quibbling over whether it is easy or hard to translate the high-level proof into a low level proof, since in principle it will always be possible to do this.
Best Answer
Time to mention the Selected Papers Network: https://selectedpapers.net
EDIT:
I hope that Tim does not mind me editing this to add extra links:
Introductory discussion by John Baez: http://johncarlosbaez.wordpress.com/2013/06/14/the-selected-papers-network-part-2/
Introductory discussion by Tim Gowers: http://gowers.wordpress.com/2013/06/16/the-selected-papers-network/#more-4954