simp only [Set.mem_insert_iff, true_or]
case mpr.intro.right.a
α : 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
⊢ ~p ∈ insert (~p) (□''⁻¹^[n]Ω.theory)
no goals