intro h hn
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
⊢ p ∈ maximalConsistentTheory consisT → ~p ∉ maximalConsistentTheory consisT
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : p ∈ maximalConsistentTheory consisT
hn : ~p ∈ maximalConsistentTheory consisT
⊢ False