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