[FOM] Is there a higher order Takeuti conjecture?

[Colin McLarty]

Takeuti in 1953 conjectured that a sequent formalisation of
second-order logic has cut-elimination,.  It was proved a good while
later by Tait, and Takahashi, and later Girard.

Is there an analogue, known or still open, for sequent formalisations
of third and higher-order logic?

thanks, Colin