simp [ValidOnModel]
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
V : ClassicalValuation α
⊢ ClassicalModel V ⊧ p ↔ V ⊧ p
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
V : ClassicalValuation α
⊢ (∀ (w : (ClassicalModel V).World), Satisfies (ClassicalModel V) w p) ↔ Satisfies (ClassicalModel V) PUnit.unit p