simp_all
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
hp : ⊥ ∈ maximalConsistentTheory consisT
this✝ : Inconsistent (maximalConsistentTheory consisT)
this : ¬Consistent (maximalConsistentTheory consisT)
⊢ False
no goals