Lean is the calculus of inductive constructions with uniqueness of identity proofs. Classical logic in Lean requires using axioms.