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