Theorem: church_rosser_implies_confluent (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ church_rosser R → confluent R
Tactic:
intros cr y z wedge
State after:
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

State before:
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
Tactic:
aesop
State after:
no goals