intro h p hp
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[n] Ω₂ → ∀ {p : Formula α}, p ∈ □''⁻¹^[n]Ω₁.theory → p ∈ Ω₂.theory
case mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
h : Ω₁ ≺^[n] Ω₂
p : Formula α
hp : p ∈ □''⁻¹^[n]Ω₁.theory
⊢ p ∈ Ω₂.theory