Proving parametricity for Gallina functions
My belief has always been that you cannot prove such free theorems from within Gallina about Gallina terms, but I don't have a definite reason why. I certainly can't imagine how this proof would work, given that there's no way to analyze functions like instances of nat' other than applying them.

As you mentioned, you can (in principle) do a parametricity proof for a deeply-embedded language.