cases' wedge with w h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x y : A
wedge : _root_.wedge R x y
⊢ joins R x y
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x y w : A
h : refl_trans_clos R w x ∧ refl_trans_clos R w y
⊢ joins R x y