simp [Kripke.Satisfies]
case hatom
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
a : α
⊢ ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ atom a ↔ atom a ∈ Ω.theory
no goals