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