Even if you "believe" in LEM, I think it could be helpful to conceptualize proofs that use it as instead being proofs in the "Reader monad" over LEM. So instead

Even if you "believe" in LEM, I think it could be helpful to conceptualize proofs that use it as instead being proofs in the "Reader monad" over LEM. So instead of proving `A => B`, you prove `A => Reader[LEM, B] = A => (LEM => B)`. If you really examine the proof you're doing, probably you don't need LEM in its full power, but actually some specific `Not[Not[X]] => X` (or a handful of specific instances like that). The neat thing about this is that in principle it could be tracked in a proof assistant with type inference. The ZIO framework for Scala has a super slick system for dependencies where e.g. an `RIO[Foo,A]` (an IO that requires a Foo and returns an A) and `A => RIO[Bar,B]` can compose to form an RIO[Foo&Bar, B] with the types inferred. So you could in principle have a proof system that lets you infer types like `A => Reader[LEM[Foo] & LEM[Bar], B]` (where LEM[T] = Not[Not[T]] => T), i.e. you get explicit types that show all of the instances of an LEM function you need to make your proof constructive, and since you're thinking of things as living in the Reader monad, you have the ergonomics of a proof that just assumes LEM. Same idea could be used with AC or any other "controversial" axiom. So you don't need to "believe" them to use them, and if you do "believe" them, you can benefit from pretending you don't.