induction n generalizing Ω₁ Ω₂ with
| zero =>
  simp_all;
  constructor;
  . intro h; subst h; tauto;
  . intro h; apply intro_equality; simpa;
| succ n ih =>
  constructor;
  . simp;
    intro Ω₃ h₁₃ h₃₂ p h;
    exact ih.mp h₃₂ $ h₁₃ h;
  . intro h;
    obtain ⟨Ω, hΩ⟩ := lindenbaum (L := L) (T := (□''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory)) $ by
      apply intro_union_ParametricConsistent;
      intro Γ Δ hΓ hΔ hC;
      replace hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory := by simpa using hΓ;
      have dΓconj : Ω₁.theory *⊢[L]! □Γ.conj' := membership_iff.mp $ iff_mem_box_conj'.mpr hΓ;
      have hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory := by
        intro p hp;
        simpa using hΔ (◇^[n]p) (by simp_all);
      have hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory := iff_mem_conj'.mpr hΔ₂;
      have : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj') := imp_trans! (andImplyIffImplyImply'!.mp hC)
        $ contra₂'! $ imp_trans! (conj₂'! multidiaDuality!)
        $ imp_trans! iff_conj'multidia_multidiaconj'! $ by
          apply conj'conj'_subset;
          intro q hq;
          obtain ⟨r, _, _⟩ := by simpa using hΔ q hq;
          subst_vars;
          simpa;
      have : L ⊢! □Γ.conj' ⟶ □^[(n + 1)](~(◇'⁻¹^[n]Δ).conj') := by simpa only [UnaryModalOperator.multimop_succ] using imply_box_distribute'! this;
      have : (◇'⁻¹^[n]Δ).conj' ∉ Ω₂.theory := iff_mem_neg.mp $ h $ membership_iff.mpr $ (Context.of! this) ⨀ dΓconj;
      contradiction;
    existsi Ω;
    constructor;
    . intro p hp;
      apply hΩ;
      simp_all;
    . apply ih.mpr;
      apply multibox_multidia.mpr;
      intro p hp;
      apply hΩ;
      simp_all;
α : 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 α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
no goals