apply iff_definability_memAxiomSetFrameClass AxiomSet.EFQ.definability |>.mpr
case left
α : Type
inst✝ : Inhabited α
⊢ LEMCounterexampleModel.Frame ∈ 𝔽(𝗘𝗙𝗤)
case left
α : Type
inst✝ : Inhabited α
⊢ True