obtain ⟨w₁, w₂, r₁₂, w₃, r₂₃, nr₁₃⟩ := hT
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hT : ∃ x x_1, F.Rel x x_1 ∧ ∃ x_2, F.Rel x_1 x_2 ∧ ¬F.Rel x x_2
⊢ ¬F ⊧* 𝗟
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
⊢ ¬F ⊧* 𝗟