intros
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
⊢ ∀ (V : Valuation F.World α) (h : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V w₁ a → V w₂ a),
    ValidOnModel { Frame := F, Valuation := V, hereditary := h } ((p ⟶ r) ⟶ (q ⟶ r) ⟶ p ⋎ q ⟶ r)
α : Type u_1
inst✝ : Inhabited α
F : Frame' α
p q r : Formula α
V✝ : Valuation F.World α
h✝ : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : α}, V✝ w₁ a → V✝ w₂ a
⊢ ValidOnModel { Frame := F, Valuation := V✝, hereditary := h✝ } ((p ⟶ r) ⟶ (q ⟶ r) ⟶ p ⋎ q ⟶ r)