simp [*] at r_x_y
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
r_x_y : RX x y
r_x_z : RX x z
⊢ joins RX y z
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
r_x_y : x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
r_x_z : RX x z
⊢ joins RX y z