Not all proof assistants are based on dependent type theory. The HOL family is based on simple type theory + a classical axioms: you get choice, excluded middle

Not all proof assistants are based on dependent type theory. The HOL family is based on simple type theory + a classical axioms: you get choice, excluded middle, extensionality etc. in exchange for a less powerful type system. Maybe not coincidentally, Isabelle/HOL also has arguably the most powerful automation thanks to its ability to call automatic provers, almost all of which are based on non-dependent classical logic. Other non-dependent type theory systems are Mizar, the B method, TLAps…