intros semi x y wedge
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ semi_confluent R → confluent R
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