intro h Ω' hΩ'
case hbox.mpr
α : 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 ∈ Ω.theory → Ω ⊧ □p
case hbox.mpr
α : 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
h : □p ∈ Ω.theory
Ω' : (CanonicalModel L).Frame.World
hΩ' : Ω ≺ Ω'
⊢ Kripke.Satisfies (CanonicalModel L) Ω' p