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