• Robbert Krebbers's avatar
    Simplify proof of auth_local_update. · ce32b224
    Robbert Krebbers authored
    Also, use explicit unfolding lemmas for auth_valid and auth_validN.
    The `Arguments valid _ _ !_ /` hack did not really work when one
    has to deal with the valid instance of the cmra, which underneath also
    includes a `cmra_valid`. Declaring a similar Arguments for `cmra_valid`
    is a bad idea, it will also end up unfold stuff for the exclusive and
    option CMRA.
    ce32b224
auth.v 13.1 KB