proposition: Lemma confluent_nf_r x y : confluent R → rtsc R x y → nf R y → rtc R x y.
proof: Proof. rewrite confluent_alt. intros Hcr ??. destruct (Hcr x y) as (z&Hx&Hy); auto. by apply rtc_nf in Hy as ->. Qed.
imports: stdpp(options)