exact mem_maximalConsistentTheory_iff.mp
  (by simpa [hp] using mem_or_neg_mem_maximalConsistentTheory (consisT := consisT) p)
case neg
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∉ maximalConsistentTheory consisT
⊢ maximalConsistentTheory consisT ⊢! ~p
no goals