intros cr y z wedge
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ church_rosser R → confluent R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
cr : church_rosser R
y z : A
wedge : _root_.wedge R y z
⊢ joins R y z