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