intros red_x_y joins_y_z
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
⊢ R x y → joins R y z → joins R x z
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
joins_y_z : joins R y z
⊢ joins R x z