A bit of a hair-splitting, but isn't explicit construction the only way formal theorem provers can work? Of course you can still prove stuff with them, but certain axioms that more "human" proofs use may not be available, like law of excluded middle (every proposition is either true or false)

(Okay, they can be made available in a way similar to `unsafe` in rust)