Proving parametricity for Gallina functions I have the following definitions

Definition nat'' {X : Type} := (X -&gt; X) -&gt; X -&gt; X.
Definition nat' := forall (X : Type), @nat'' X.


And when I wanted to prove a certain property I ended up in the following situation:

  m : nat'
  H : 0 = m nat S 0
  X : Type
  s : X -&gt; X
  z : X
  ============================
  m X s z = z


which should be some kind of free theorem! Specifically, m: (forall X : Type), (X -&gt; X) -&gt; X -&gt; X is a function that should behave parametrically for any instantiation of X, so by knowing that 0 = m nat S 0 I should be able to deduce that x = m X f x for any x : X and f : X -&gt; X.

But I haven't seen such free theorems stated in Coq for Gallina terms. Is there an easy way to go about proving such a result without some deep embedding of a language and proving parametricity for this language?
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.