Possibly confusing naming: auth_own_valid.
I was wondering if anyone else found this a bit confusing.
auth_own_valid refers to two things:
base_logic.lib.auth.auth_own_validwhich states that
own γ (◯ a) ⊢ ✓ a;
algebra.auth.auth_own_validwhich (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.