have : R y z := trans (symm ‹R x y›) ‹R x 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 y z
⊢ False