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