. intros h
  apply not_joins_a_d
  apply h
  exists X.b; constructor
  . constructor
    simp [RX]
    left; trivial
    constructor
  . constructor
    simp [RX]
    right; trivial
    constructor
    . simp [RX]; right; trivial
    . constructor
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ¬confluent RX
no goals