Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.classical_iff (Logic/Propositional/Superintuitionistic/Kripke/Classical.lean)

State before:
α : Type u_1
inst✝ : Inhabited α
p q : Formula α
V : ClassicalValuation α
⊢ ClassicalModel V ⊧ p ↔ V ⊧ p
Tactic:
simp [ValidOnModel]
State after:
α : 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

State before:
α : 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
Tactic:
tauto
State after:
no goals