proposition: Lemma tclosure_eq_tclosure'l : forall R, tclosure R = tclosure'l R.
proof: Proof. Proof using. extens. intros x y. iff M. { induction* M. applys* trans_tclosure'l y. } { induction* M. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)