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