have : R x y := trans ‹R x z› (symm ‹R y z›)
α : Sort u
R : α → α → Prop
inst✝¹ : Symmetric R
inst✝ : Transitive R
x y z : α
x✝² : ¬R x y
x✝¹ : R y z
x✝ : R x z
⊢ False
α : Sort u
R : α → α → Prop
inst✝¹ : Symmetric R
inst✝ : Transitive R
x y z : α
x✝² : ¬R x y
x✝¹ : R y z
x✝ : R x z
this : R x y
⊢ False