by_cases hp : p ∈ maximalConsistentTheory consisT <;> simp[hp]
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
⊢ p ∉ maximalConsistentTheory consisT ↔ maximalConsistentTheory consisT ⊢! ~p
case pos
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∈ maximalConsistentTheory consisT
⊢ ¬maximalConsistentTheory consisT ⊢! ~p

case neg
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
hp : p ∉ maximalConsistentTheory consisT
⊢ maximalConsistentTheory consisT ⊢! ~p