proposition: Lemma trans_rtclosure'l : forall R, trans (rtclosure'l R).
proof: Proof. Proof using. Hint Constructors rtclosure'l. intros R y x z M1. gen z. induction M1; introv M2; autos*. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)