proposition: Lemma sclosure_inverse_eq : forall R, sclosure (inverse R) = sclosure R.
proof: Proof. Proof using. unfolds inverse. extens. intros. do 2 rewrite sclosure_eq. autos*. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)