proposition: Lemma church_rosser (R: X -> X -> Prop) s t: confluent R -> equiv R s t -> exists v: X, star R s v /\ star R t v.
proof: Proof. induction 2. - now (exists x). - inv H0. + destruct IHstar as [v]; exists v; intuition; eauto. + destruct IHstar; intuition. edestruct H. eapply H3. econstructor 2; eauto. exists x1; split; eauto. Qed.
imports: Morphisms FinFun Undecidability.HOU(std.tactics std.misc std.ars.basic)