proposition: Lemma tclosure_of_rtclosure_l : forall R x y z, rtclosure R x y -> R y z -> tclosure R x z.
proof: Proof. Proof using. introv H M. destruct (rtclosure_inv_rclosure_or_tclosure H). { subst*. } { applys* tclosure_r. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)