induction red_x_y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y : A
red_x_y : refl_trans_sym_clos R x y
⊢ joins R x y
case refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y a✝ : A
⊢ joins R a✝ a✝

case base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y a✝¹ b✝ : A
a✝ : R a✝¹ b✝
⊢ joins R a✝¹ b✝

case trans
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y a✝² b✝ c✝ : A
a✝¹ : refl_trans_sym_clos R a✝² b✝
a✝ : refl_trans_sym_clos R b✝ c✝
a_ih✝¹ : joins R a✝² b✝
a_ih✝ : joins R b✝ c✝
⊢ joins R a✝² c✝

case inv
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y a✝¹ b✝ : A
a✝ : refl_trans_sym_clos R b✝ a✝¹
a_ih✝ : joins R b✝ a✝¹
⊢ joins R a✝¹ b✝