. exists X.a; repeat constructor
case left.inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.a
h✝ : z = X.a
⊢ 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) X.a X.a

case left.inl.inr
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
⊢ 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) X.a z

case left.inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ 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 X.a

case left.inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.b ∧ z = X.c ∨ 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
case left.inl.inr
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
⊢ 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) X.a z

case left.inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ 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 X.a

case left.inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.b ∧ z = X.c ∨ 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