cases either_consistent Ω.consistent p with
| inl h => have := Ω.maximal (Set.ssubset_insert hC.1); contradiction;
| inr h => have := Ω.maximal (Set.ssubset_insert hC.2); contradiction;
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : p ∉ Ω.theory ∧ ~p ∉ Ω.theory
⊢ False
no goals