intros y z wedge
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
⊢ confluent R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
y z : A
wedge : _root_.wedge R y z
⊢ joins R y z