proposition: Lemma rel_incl_rclosure_rtclosure : forall R, rel_incl (rclosure R) (rtclosure R).
proof: Proof. Proof using. intros. applys* rtclosure_of_rclosure. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)