right
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
case right.a.right.a.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.right.a.b = X.d