Perennial has a simple ghost-var library based on excl_auth, but it turns out in one case they need a fraction, and at some point IMO generalizing excl_auth further is the wrong approach -- one should just use frac * agree A as the underlyoing algebra. I think it is not worth having an algebra lib for this though, so I propose we have a very simple logic-level library for this. It can also serve as an example for how to "lift" an RA into the logic.
@tchajed I think this can fully replace the ghost_var lib in Perennial (unless I forgot some lemma).