proposition: Theorem WeakConfluence_is_ChurchRosser0': WeakConfluence -> ChurchRosser.
proof: Proof. intros H p q Hpq. induction Hpq as [p | p q q' Hpq Hqq' IH]. eexists; constructor. destruct Hpq as [Hpq|Hpq]. destruct IH as [s' Hqs' Hs'q']. destruct (H p q s' Hpq Hqs'). eauto 6 using trans_rt1n, rt_trans, rt1n_trans. destruct IH as [s Hqs Hsq']. eauto using Relation_Operators.rt1n_trans. Qed.
imports: ATBR(ATBR) Coq(Relations)