proposition: Lemma tclosure_sclosure_eq_stclosure : forall R, tclosure (sclosure R) = stclosure R.
proof: Proof. Proof using. extens. intros x y. iff M. { induction* M. { applys* stclosure_of_sclosure. } } { induction* M. { applys* sym_inv. } } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)