Made refcell state coercion implementation agnostic

This MR changes how some shorthand notation for the refcell state type was declared as a Coercion in Coq.
In particular, it makes the coercion work with iris!971, but it is also shorter and (in my opinion) more readable.