obtain ⟨Ω', hΩ'⟩ := lindenbaum (L := L) (T := insert (~p) (□''⁻¹^[n]Ω.theory)) (by
  apply unprovable_iff_insert_neg_ParametricConsistent.mp;
  by_contra hC;
  obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp hC;
  have : L ⊢! □^[n]Γ.conj' ⟶ □^[n]p := imply_multibox_distribute'! $ implyLeft_conj_eq_conj'!.mp hΓ₂;
  have : L ⊬! □^[n]Γ.conj' ⟶ □^[n]p := by
    have := Context.provable_iff.not.mp $ membership_iff.not.mp hp;
    push_neg at this;
    have : L ⊬! (□'^[n]Γ : List (Formula α)).conj' ⟶ □^[n]p := implyLeft_conj_eq_conj'!.not.mp $ FiniteContext.provable_iff.not.mp $ this (□'^[n]Γ) (by
      intro q hq;
      obtain ⟨r, hr₁, hr₂⟩ := by simpa using hq;
      subst hr₂;
      simpa using hΓ₁ r hr₁;
    );
    revert this;
    contrapose;
    simp [neg_neg];
    exact imp_trans! collect_multibox_conj'!;
  contradiction;
)
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
⊢ ∃ Ω', □''⁻¹^[n]Ω.theory ⊆ Ω'.theory ∧ p ∉ Ω'.theory
case mpr.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
hp : □^[n]p ∉ Ω.theory
Ω' : MCT L
hΩ' : insert (~p) (□''⁻¹^[n]Ω.theory) ⊆ Ω'.theory
⊢ ∃ Ω', □''⁻¹^[n]Ω.theory ⊆ Ω'.theory ∧ p ∉ Ω'.theory