A proof of cut-elimination theorem in simple type-theory

Abstract

In [4], G. Takeuti cor1jectured that the cut-elimination theorem would hold in his system GLC as well as in LK. Many attempts to prove it constructively