intro (_ : ¬ R x y) (_ : R y z) (_ : R x z)
α : Sort u
R : α → α → Prop
inst✝¹ : Symmetric R
inst✝ : Transitive R
x y z : α
⊢ ¬R x y → R y z → ¬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