intro Ω
case hbox
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
⊢ ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ □p ↔ □p ∈ Ω.theory
case hbox
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
ih : ∀ {Ω : (CanonicalModel L).World}, Ω ⊧ p ↔ p ∈ Ω.theory
Ω : (CanonicalModel L).World
⊢ Ω ⊧ □p ↔ □p ∈ Ω.theory