exact hpr (M.Frame.Rel_trans hw₂₃ hw₃₄) hp
case inl
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
w₁ : M.World
w₂ : M.Frame.World
a✝ : w₁ ≺ w₂
hpr : ∀ {w' : M.Frame.World}, w₂ ≺ w' → Satisfies M w' p → Satisfies M w' r
w₃ : M.Frame.World
hw₂₃ : w₂ ≺ w₃
hqr : ∀ {w' : M.Frame.World}, w₃ ≺ w' → Satisfies M w' q → Satisfies M w' r
w₄ : M.Frame.World
hw₃₄ : w₃ ≺ w₄
hp : Satisfies M w₄ p
⊢ Satisfies M w₄ r
no goals