proposition: Lemma rtclosure_inverse_eq : forall R, rtclosure (inverse R) = inverse (rtclosure R).
proof: Proof. Proof using. unfold inverse. extens. iff M; induction* M. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)