simpa [ValidOnFrameClass, ValidOnFrame, ValidOnModel] using not_imp_not.mpr complete! hnq
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬𝐈𝐧𝐭 ⊢! p ∧ ¬𝐈𝐧𝐭 ⊢! q
hnp : ¬𝐈𝐧𝐭 ⊢! p
hnq : ¬𝐈𝐧𝐭 ⊢! q
Fp : Frame' α
left✝ : Fp ∈ 𝔽(𝗘𝗙𝗤)
Vp : Valuation Fp.World α
hVp : ∀ {w₁ w₂ : Fp.World}, w₁ ≺ w₂ → ∀ {a : α}, Vp w₁ a → Vp w₂ a
wp : { Frame := Fp, Valuation := Vp, hereditary := ⋯ }.World
hp : ¬Satisfies { Frame := Fp, Valuation := Vp, hereditary := ⋯ } wp p
⊢ ?m.515393
no goals