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