. constructor
  simp [RX]
  right; trivial
  constructor
  . simp [RX]; right; trivial
  . constructor
case right.a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.d
no goals