intro Ω' hΩ'
case hbox.mp
α : 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
⊢ ∀ {Ω' : MCT L}, □''⁻¹Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
case hbox.mp
α : 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
Ω' : MCT L
hΩ' : □''⁻¹Ω.theory ⊆ Ω'.theory
⊢ p ∈ Ω'.theory