proposition: Lemma tclosure_eq_of_trans : forall R, trans R -> tclosure R = R.
proof: Proof. Proof using. unfolds trans. introv H. extens. iff M. { induction M; subst*. } { auto. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)