have : Inconsistent (maximalConsistentTheory consisT) :=
  System.inconsistent_iff_provable_bot.mpr
    (by prover [mem_maximalConsistentTheory_iff.mp h, mem_maximalConsistentTheory_iff.mp hn])
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : p ∈ maximalConsistentTheory consisT
hn : ~p ∈ maximalConsistentTheory consisT
⊢ False
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : p ∈ maximalConsistentTheory consisT
hn : ~p ∈ maximalConsistentTheory consisT
this : Inconsistent (maximalConsistentTheory consisT)
⊢ False