have b : maximalConsistentTheory consisT ⊢! ~p ∧ maximalConsistentTheory consisT ⊢! ~q := by
  simpa [not_or, not_mem_maximalConsistentTheory_iff] using A
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
h : p ⋎ q ∈ maximalConsistentTheory consisT
A : ¬(p ∈ maximalConsistentTheory consisT ∨ q ∈ maximalConsistentTheory consisT)
⊢ False
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
h : p ⋎ q ∈ maximalConsistentTheory consisT
A : ¬(p ∈ maximalConsistentTheory consisT ∨ q ∈ maximalConsistentTheory consisT)
b : maximalConsistentTheory consisT ⊢! ~p ∧ maximalConsistentTheory consisT ⊢! ~q
⊢ False