case hnatom =>
  simpa using maximalConsistentTheory_consistent' hp
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
a✝ : α
hp : Formula.natom a✝ ∈ maximalConsistentTheory consisT
⊢ Formula.atom a✝ ∉ maximalConsistentTheory consisT
no goals