. simp [*]; constructor; simp [RX]
  . left; trivial
  . constructor; simp [RX]; left; trivial; constructor
case left.inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) z X.a
no goals