no goals
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w
inst✝ : Structure L M
φ : Sentence L
⊢ φ ∈ completeTheory L M ∨ Formula.not φ ∈ completeTheory L M
simp_rw [completeTheory, Set.mem_setOf_eq, Sentence.Realize, Formula.realize_not, or_not]