. contrapose;
  push_neg;
  intro hp;
  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;
  );
  existsi Ω';
  constructor;
  . exact Set.Subset.trans (by simp_all) hΩ';
  . apply iff_mem_neg.mp;
    apply hΩ';
    simp only [Set.mem_insert_iff, true_or]
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory) → □^[n]p ∈ Ω.theory
no goals