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
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h1 : x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h2 : x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (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) y z
no goals