. apply iff_mem_imp.not.mpr; simp [hpY, hqY];
case h.right
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ □p ⟶ q ∉ Y.theory
no goals