[GregarianChild]

HOL is typed, but not a dependent type theory. HOL is also a classical logic. HOL is essentially Alonzo Church's simply typed lambda-calculus [1] from 1940. Classical, rather than constructive logic tends to give shorter proofs.

[1] A. Church, A Formulation of the Simple Theory of Types. https://pdfs.semanticscholar.org/28bf/123690205ae5bbd9f8c84b...