proposition: Lemma trans_rclosure : forall R, trans R -> trans (rclosure R).
proof: Proof. Proof using. unfolds trans. introv H M1 M2. destruct M1; destruct M2; subst*. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)