simp_all [ValidOnFrameClass, ValidOnFrame, ValidOnModel]
case hDisj₃
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ r✝ : Formula α
⊢ 𝔽(Ax(L)) ⊧ (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
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✝