revert h2 y
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ joins R x y
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x w : A
h1 : refl_trans_clos R w x
⊢ ∀ (y : A), refl_trans_clos R w y → joins R x y