add counterexample for uPred CMRA extension axiom

@robbertkrebbers asked about this old counterexample that I posted on the iris-club mailing list in 2016, and since it took some time to find, I figured maybe we should have it in a place that is easier to discover.

Thanks for digging up this proof! I think it's a correct proof (but I'm way less competent at proof checking than Coq, so don't necessarily trust me...).

It would be nice to Coqdoc-ify this comment.

added 1 commit

• 7dd6d84e - apply feedback

Compare with previous version

resolved all threads

I used coqdoc for inline formulas in the text, but I have no idea how the larger formula blocks will look.

Thanks :)

Preformatted vernacular is enclosed by [[ and ]]. The former must be followed by a newline and the latter must follow a newline.

https://coq.inria.fr/distrib/current/refman/using/tools/coqdoc.html#coq-material-inside-documentation

added 1 commit

• 33d0c3c6 - apply feedback; use more coqdoc

Compare with previous version

Thanks for figuring that out! I applied this. Merging then.

merged

mentioned in commit 5558d66d