case hfalsum =>
  have : Inconsistent (maximalConsistentTheory consisT) := System.inconsistent_of_provable ⟨System.byAxm hp⟩
  have := this.not_con
  simp_all
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
hp : ⊥ ∈ maximalConsistentTheory consisT
⊢ False
no goals