simp only [iff_mem_multibox, iff_mem_conj']
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ □^[n]Γ.conj' ∈ Ω.theory ↔ ∀ p ∈ Γ, □^[n]p ∈ Ω.theory
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory) ↔
    ∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory