proposition: Theorem WeakConfluence_is_ChurchRosser0: WeakConfluence -> ChurchRosser.
proof: Proof. intros H p q Hpq. induction Hpq as [p | p q q' Hpq Hqq' IH]. exists p. constructor. constructor. destruct Hpq as [Hpq|Hpq]. destruct IH as [s' Hqs' Hs'q']. destruct (H p q s' Hpq Hqs') as [s Hps Hss']. exists s. assumption. apply trans_rt1n. apply rt_trans with s'; apply rt1n_trans; assumption. destruct IH as [s Hqs Hsq']. exists s. apply Relation_Operators.rt1n_trans with q; assumption. assumption. Qed.
imports: ATBR(ATBR) Coq(Relations)