proposition: Lemma rclosure_tclosure_eq_rtclosure : forall R, rclosure (tclosure R) = rtclosure R.
proof: Proof. Proof using. extens. intros x y. iff M. { induction* M. { applys* rtclosure_of_tclosure. } } { induction* M. { destruct IHM1; destruct IHM2; autos*. } } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)