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