proposition: Lemma sclosure_rclosure_eq_rsclosure : forall R, sclosure (rclosure R) = rsclosure R.
proof: Proof. Proof using. extens. intros x y. iff M. { induction* M. { applys* rsclosure_of_rclosure. } } { induction* M. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)