exact validOnAxiomSetFrameClass_axiom h hF
case eaxm
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ : Formula α
h : p✝ ∈ Ax(𝓓)
⊢ F ⊧ p✝
no goals