proposition: Lemma tclosure_eq_of_refl_trans : forall R, refl R -> trans R -> rtclosure R = R.
proof: Proof. Proof using. unfolds refl, trans. introv H1 H2. extens. iff M. { induction M; subst*. } { autos*. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)