The _op etc should be a suffix.
What this MR does not fix is the inconsistency between the f_op lemmas on the one side and the f_core/f_included lemmas on the other side: the former have the "operation at the result type of f" (so, e.g. the composition of gmaps, for the singleton_ lemmas) on the right-hand side, while the latter have it on the left-hand side.
Cc @iris-users because this is a breaking change, but should be fairly easy to fix.