intros
case hDisj₃
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
⊢ ∀ F ∈ 𝔽(Ax(L)),
    ∀ (V : Valuation F.World α) (w : { Frame := F, Valuation := V }.World),
      (Satisfies { Frame := F, Valuation := V } w p✝ → Satisfies { Frame := F, Valuation := V } w r✝) →
        (Satisfies { Frame := F, Valuation := V } w q✝ → Satisfies { Frame := F, Valuation := V } w r✝) →
          Satisfies { Frame := F, Valuation := V } w p✝ ∨ Satisfies { Frame := F, Valuation := V } w q✝ →
            Satisfies { Frame := F, Valuation := V } w r✝
case hDisj₃
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
F✝ : Frame' α
a✝³ : F✝ ∈ 𝔽(Ax(L))
V✝ : Valuation F✝.World α
w✝ : { Frame := F✝, Valuation := V✝ }.World
a✝² : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
a✝¹ : Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
a✝ : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ ∨ Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝
⊢ Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝