proposition: Lemma rel_incl_tclosure_stclosure_l : forall R1 R2, rel_incl R1 (stclosure R2) -> rel_incl (tclosure R1) (stclosure R2).
proof: Proof. Proof using. introv H M. induction* M. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)