apply h
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ joins RX X.a X.d
case right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ wedge RX X.a X.d