prover [mem_maximalConsistentTheory_iff.mp hp, bnp]
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∈ maximalConsistentTheory consisT
bnp : maximalConsistentTheory consisT ⊢! ~p
⊢ maximalConsistentTheory consisT ⊢! ⊥
no goals