Direction of _op lemmas is inconsistent with _(p)core, _valid, _included
See the discussion at !403 (comment 47448): our _(p)core, _valid, _included lemmas generally push the named operation "in", e.g.
Lemma pair_valid (a : A) (b : B) : ✓ (a, b) ↔ ✓ a ∧ ✓ b.
Lemma pair_core `{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
core (a, b) = (core a, core b).However, most of our _op lemmas push the named operation "out":
Lemma pair_op (a a' : A) (b b' : B) : (a ⋅ a', b ⋅ b') = (a, b) ⋅ (a', b').Moreover, even with one "group" of lemmas, not all are consistent: singleton_op, discrete_fun_singleton_op, list_singleton_op push "in", while cmra_morphism_(p)core push "out" (and there might be more).
At the very least, we should make all lemmas within a "group" consistent. So, the minimal fix for this is to swap the 5 lemmas named in the last paragraph. However, we might also want to fix the larger inconsistency that the _op lemmas are going the other way, compared to the rest of them. The thing is, we already swapped half of them !303 (merged), so this starts to look like we are just going back and forth...