simpa [not_or] using A
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
⊢ p ∉ maximalConsistentTheory consisT ∧ ~p ∉ maximalConsistentTheory consisT
no goals