simp [RX]
case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ RX X.c ?right.a.right.a.b
case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.right.a.b = X.b ∨ ?right.a.right.a.b = X.d