--unabbreviate=R

R removal is useful to interface with tools such as Rabinizer 3, that have no support for R.

If we have support for unabbreviating R, W, and M, it probably also makes sense to implement several rewriting rules depending on the operators we are allowed to use. See Appendix A of tl.pdf.