GitLab

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 Jun 21, 2019 and Ralf Jung committed Jun 21, 2019

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