simpa [hp] using mem_or_neg_mem_maximalConsistentTheory (consisT := consisT) p
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∉ maximalConsistentTheory consisT
⊢ ~p ∈ maximalConsistentTheory consisT
no goals