have : Inconsistent (maximalConsistentTheory consisT) :=
  System.inconsistent_of_provable (by prover [mem_maximalConsistentTheory_iff.mp hp, bnp])
case pos
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∈ maximalConsistentTheory consisT
bnp : maximalConsistentTheory consisT ⊢! ~p
⊢ False
case pos
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∈ maximalConsistentTheory consisT
bnp : maximalConsistentTheory consisT ⊢! ~p
this : Inconsistent (maximalConsistentTheory consisT)
⊢ False