have : Inconsistent (maximalConsistentTheory consisT) := System.inconsistent_of_provable ⟨System.byAxm hp⟩
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
hp : ⊥ ∈ maximalConsistentTheory consisT
⊢ False
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
hp : ⊥ ∈ maximalConsistentTheory consisT
this : Inconsistent (maximalConsistentTheory consisT)
⊢ False