exact contra₁'! $ conj₁'! $ multidiaDuality!
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝² : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝¹ : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝ : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
⊢ L ⊢! □^[t.n](~Γ.conj') ⟶ ~(◇^[t.n]Γ.conj')
no goals