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