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