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