proposition: Lemma trans_rclosure_l : forall y x z R, trans R -> rclosure R x y -> R y z -> R x z.
proof: Proof. Proof using. introv T M H. rewrite rclosure_eq in *. destruct M; subst*. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)