proposition: Lemma rtclosure_eq_rtclosure'l : forall R, rtclosure R = rtclosure'l R.
proof: Proof. Proof using. extens. intros x y. iff M. { induction* M. applys* trans_rtclosure'l y. } { induction* M. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)