intro Ω₃ h₁₃ h₃₂ p 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
⊢ ∀ (x : MCT L),
    (∀ {p : Formula α}, □p ∈ Ω₁.theory → p ∈ x.theory) →
      RelItr (fun x x_1 => ∀ {p : Formula α}, □p ∈ x.theory → p ∈ x_1.theory) n x Ω₂ →
        ∀ {p : Formula α}, UnaryModalOperator.mop true ((UnaryModalOperator.mop true)^[n] p) ∈ Ω₁.theory → p ∈ Ω₂.theory
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
Ω₃ : MCT L
h₁₃ : ∀ {p : Formula α}, □p ∈ Ω₁.theory → p ∈ Ω₃.theory
h₃₂ : RelItr (fun x x_1 => ∀ {p : Formula α}, □p ∈ x.theory → p ∈ x_1.theory) n Ω₃ Ω₂
p : Formula α
h : UnaryModalOperator.mop true ((UnaryModalOperator.mop true)^[n] p) ∈ Ω₁.theory
⊢ p ∈ Ω₂.theory