Draft: experiment: use coq's ability to infer more canonical structures

I wonder if we should recommend this style, once all Coq versions we support can handle it. It is certainly much nicer, we could entirely hide these R/UR terms from users. Unfortunately in one case already in this repo, it requires more type annotations. I don't understand why Coq cannot infer that any more.