Remove an unused argument for `newcounter_mono_spec`.
The monotonic counter does not really assert ownership of any propositions, so R : iProp \Sigma
is just a dangling argument to newcounter_mono_spec
.
The monotonic counter does not really assert ownership of any propositions, so R : iProp \Sigma
is just a dangling argument to newcounter_mono_spec
.