Turn all `f_op` lemmas to have shape `f (x ⋅ y) = f x ⋅ f y`, following the plan
in iris/iris!295 (comment 39151), plus
`cmra_morphism_op`.

- And use prop_ext instead of prop_ext_2 in other proofs.

Paolo G. Giarrusso authored 5 years ago and Ralf Jung committed 5 years ago

On Mac, options must come first. On Linux this should still be fine, and works
with gnu-sed.

docs: for now we won't document atomic triples or total triples; de-experimentalize plainly and stuckness