. intros x y z r_x_y r_x_z
  simp [*] at r_x_y
  simp [*] at r_x_z
  cases r_x_y <;> cases r_x_z <;> simp [*] at *
  . exists X.a; repeat constructor
  . exists X.a; try constructor
    . constructor
    . simp [*]; constructor; simp [RX]
      . left; trivial
      . constructor; simp [RX]; left; trivial; constructor
  . exists X.a; simp [*]; constructor
    . repeat (constructor; simp [RX]; left; trivial)
      constructor
    . constructor
  . case inr h1 h2 =>
    cases h1 <;> cases h2 <;> simp [*] at *
    . exists X.c; repeat constructor
    . case inr h1 h2 =>
      cases h1 <;> cases h2 <;> simp [*] at *
      . exists X.b; repeat constructor
      . exists X.d; constructor
        . constructor; simp [RX]; right; trivial
          constructor; simp [RX]; right; trivial
          constructor
        . constructor
      . exists X.d; constructor
        . constructor
        . constructor; simp [RX]; right; trivial
          constructor; simp [RX]; right; trivial
          constructor
      . exists X.d; repeat constructor
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ weakly_confluent RX

case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ¬confluent RX
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ¬confluent RX