proposition: Lemma rel_incl_sclosure_rstclosure : forall R, rel_incl (sclosure R) (rstclosure R).
proof: Proof. Proof using. intros. applys* rstclosure_of_sclosure. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)