## 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...