I don't know as much about parametricity for dependently typed language to be fully confident about this so take this with a grain of salt. But to give an upper bound on the potential utility of internal parametricity, let me describe one effective way to work with external parametricity.
Although you cannot prove $\forall u : (\forall t.t\to t). u = \lambda x. x$ within a typical type theory, one thing you can do is, given a concrete term $u$, construct a proof of $u = \lambda x. x$ (for an extensional $=$).
More generally, given a term $t : T$, you can translate the type $T$ to its Reynolds-relation $\lceil T\rceil : T \to T \to \mathrm{Type}$ and the term $t$ to a proof $\lceil t \rceil : \lceil T\rceil\;t\;t$ (from which theorems such as the one above can be derived). For example, the paramcoq plugin does this translation in Coq. Internal parametricity is when that translation is instead definable as a function in the theory itself. But external parametricity already goes a long way.
Whenever you would apply the parametricity theorem to a variable $v : T$, add the relevant instance of that theorem as an additional assumption $v' : \lceil T \rceil\;v\;v$, and whenever $v$ gets instantiated with a concrete term $t$, invoke external parametricity to construct the required proof $\lceil t \rceil$. This bloats proofs since you're threading extra assumptions and proving obvious things, but the effort is mechanizable to a high degree. Without changing the language (by adding parametricity axioms or switching to a language that internalizes parametricity), external parametricity is at least enough to enable applications of parametricity in the style of Theorems for free!.
