intro F hF
α : Type u_1
inst✝ : Inhabited α
Ax : AxiomSet α
p : Formula α
h : p ∈ Ax
⊢ 𝔽(Ax) ⊧ p
α : Type u_1
inst✝ : Inhabited α
Ax : AxiomSet α
p : Formula α
h : p ∈ Ax
F : Frame' α
hF : F ∈ 𝔽(Ax)
⊢ F ⊧ p