proposition: Lemma rstclosure_inverse_eq : forall R, rstclosure (inverse R) = rstclosure R.
proof: Proof. Proof using. unfolds inverse. extens. intros x y. iff M; induction* M. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)