apply Formula.Kripke.ValidOnModel.classical_iff.mp
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : 𝔽(Ax(𝐂𝐥)) ⊧ p
V : ClassicalValuation α
⊢ V ⊧ p
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
h : 𝔽(Ax(𝐂𝐥)) ⊧ p
V : ClassicalValuation α
⊢ ClassicalModel V ⊧ p