obtain ⟨p, _⟩ : ∃ (p : Formula α), ¬(𝔽(Ax(𝐈𝐧𝐭))) ⊧ p ⋎ ~p := noLEM_on_frameclass
α : Type
inst✝ : Inhabited α
⊢ ∃ p, 𝐈𝐧𝐭 ⊬! p ⋎ ~p
case intro
α : Type
inst✝ : Inhabited α
p : Formula α
h✝ : ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
⊢ ∃ p, 𝐈𝐧𝐭 ⊬! p ⋎ ~p