. simp;
  intro Ω₃ h₁₃ h₃₂ p h;
  exact ih.mp h₃₂ $ h₁₃ h;
case succ.mp
α : 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
⊢ Ω₁ ≺^[n + 1] Ω₂ → ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory

case succ.mpr
α : 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
⊢ (∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n + 1] Ω₂
case succ.mpr
α : 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
⊢ (∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n + 1] Ω₂