cases hpq with
| inl hp => exact hpr hp;
| inr hq => exact hqr hq;
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
hpr : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
hqr : Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝ → Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
hpq : Satisfies { Frame := F✝, Valuation := V✝ } w✝ p✝ ∨ Satisfies { Frame := F✝, Valuation := V✝ } w✝ q✝
⊢ Satisfies { Frame := F✝, Valuation := V✝ } w✝ r✝
no goals