constructor
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ~~p ∈ Ω'.theory) ↔
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ~~p ∈ Ω'.theory) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory

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) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ~~p ∈ Ω'.theory