I'm not sure I understand the question, but doesn't this always happen? For example, if I'm going to state and prove the product rule, I'm going to write:
Proposition. $(fg)' = f'g+fg'$
And that's what I'll prove. However, in practice I will probably use
$$\frac{\partial}{\partial x}(\tau \sigma) = \left(\frac{\partial}{\partial x}\tau\right)\sigma+\tau \left(\frac{\partial}{\partial x}\sigma\right)$$
where $\tau$ and $\sigma$ are terms of type $\mathbb{R}$, and $\frac{\partial}{\partial x}$ is to be understood as the metafunction of metatype $\mathrm{Terms} \rightarrow \mathrm{Terms}$ given by $\tau \mapsto (\lambda x.\tau)'(x)$.
So I guess what I'm saying is that any time higher-order functions appear, we can expect theorems to be stated and proved "extensionally" but then used "intensionally." A good foundation should have inbuilt support for this kind of thing, in my opinion, since it is so completely widespread.
To answer question (2), "why is this dichotomy not more widely taught / appreciated", I think its because words like "formal expression" and "metafunction" are not widely taught and/or appreciated outside of logic circles. As computer-formalized mathematics becomes more widespread, this will surely change. By the way, if someone were to write a textbook called "explicit mathematics" based on the premise that we should make all these kinds of little nuances explicit, I would surely buy it, hint hint, nudge nudge :)