simp_all
case succ.mpr.intro.left.a
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
p : Formula α
hp : p ∈ □''⁻¹Ω₁.theory
⊢ p ∈ □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory
no goals