proposition: Lemma all_loop_alt x : all_loop R x ↔ ∀ y, rtc R x y → red R y.
proof: Proof. split; [eauto using all_loop_red, all_loop_rtc|]. intros H. cut (∀ z, rtc R x z → all_loop R z); [eauto|]. cofix FIX. constructor; eauto using rtc_r. Qed.
imports: stdpp(options)