pub proof fn perm_u64_with_identity(p: PermissionU64)Expand description
ensures
perm_u64_with(p, p.value()) == p,Setting a PermissionU64 to its own current value is a no-op.
pub proof fn perm_u64_with_identity(p: PermissionU64)perm_u64_with(p, p.value()) == p,Setting a PermissionU64 to its own current value is a no-op.