Gaisi Takeuti's book Proof Theory proves cut elimination for Simple Type Theory (a combined result of several researchers). Thus it proves consistency of Simple Type Theory with full comprehension in each type and with cut as a proof rule. I will abbreviate that consistency statement as Con(STT). The result of interest to me is:

Conservativity Theorem: If you extend a first order theory $T$ to $\widetilde{T}$ by adding all finite higher types (with full comprehension, and cut rule) then $\widetilde{T}$ is conservative over $T$.

My question: What metatheory is best for these results?

First, I believe that Exponential Function Arithmetic (EFA) can formalize the proof theory showing "If Con(STT) then the cut-free proof system for SST is complete." I also believe EFA can formalize the unhypothetical theorem "extending any first order theory $T$ to $\widetilde{T}$ where only cut-free proofs are used in the type theory, is conservative." I have not checked these very well and they may not be true. But I hope they are true and already known or at least already obvious to proof theorists.

Second, I believe the straightforward choice of EFA plus Con(STT) is the best metatheory for this. So we regard cut elimination for STT, and the Conservativity Theorem, as depending on Con(STT) and not as proving it. If my beliefs above are correct, then this metatheory is adequate and well suited to the task. But does some better known, or more canonical, metatheory also work?