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