proposition: Lemma locally_confluent_confluent : (∀ x, sn R x) → locally_confluent R → confluent R.
proof: Proof. intros Hsn Hcr x. induction (Hsn x) as [x _ IH]. intros y1 y2 Hy1 Hy2. destruct Hy1 as [x|x y1 y1' Hy1 Hy1']; [by eauto|]. destruct Hy2 as [x|x y2 y2' Hy2 Hy2']; [by eauto|]. destruct (Hcr x y1 y2) as (z&Hy1z&Hy2z); auto. destruct (IH _ Hy1 y1' z) as (z1&?&?); auto. destruct (IH _ Hy2 y2' z1) as (z2&?&?); eauto using rtc_transitive. Qed.
imports: stdpp(options)