Non-constructive proofs aren't problematic for theorem provers---they just have no computable interpretation. You can just assert the Law of Excluded Middle if

Non-constructive proofs aren't problematic for theorem provers---they just have no computable interpretation. You can just assert the Law of Excluded Middle if you like whenever and all of the programs "downstream" will still be checkable. You can even technically provide computable semantics to Pierce's law via call/cc.