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