proposition: Lemma rsclosure_inverse_eq : forall R, rsclosure (inverse R) = rsclosure R.
proof: Proof. Proof using. unfold inverse. extens. intros. do 2 rewrite rsclosure_eq. autos*. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)