have : Consistent (insert p (maximalConsistentTheory consisT)) :=
  consistent_insert_iff_not_refutable.mpr
    (show ~p ∉ theory (maximalConsistentTheory consisT) from by simpa using hp.2)
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
hp : p ∉ maximalConsistentTheory consisT ∧ ~p ∉ maximalConsistentTheory consisT
⊢ False
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
hp : p ∉ maximalConsistentTheory consisT ∧ ~p ∉ maximalConsistentTheory consisT
this : Consistent (insert p (maximalConsistentTheory consisT))
⊢ False