simpa
case h.intro.intro
α : 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
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
r : Formula α
left✝ : r ∈ Ω₂.theory
hq : (UnaryModalOperator.mop false)^[n] r ∈ Δ
⊢ (UnaryModalOperator.mop false)^[n] r ∈ ◇'^[n]◇'⁻¹^[n]Δ
no goals