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