Possibly confusing naming: auth_own_valid.

I was wondering if anyone else found this a bit confusing.

The lemma auth_own_valid refers to two things:

• base_logic.lib.auth.auth_own_valid which states that own γ (◯ a) ⊢ ✓ a;
• algebra.auth.auth_own_valid which (roughly) states that ✓ (● a, ◯ b) → ✓ b.

If you need both of those modules, then the order in which you import them is quite significant.

I guess the issue is that auth_own refers both to the proposition of owning the fragment part of the Auth algebra and to the actual fragment part of the algebra.