simp [Transitive] at hT
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hT : ¬Transitive F.Rel
⊢ ¬F ⊧* 𝗟
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 ⊧* 𝗟