proposing to amalgamate `HighPriotityInUnblockedQueue` and `HighPriorityHasWork`

[sophiaIC]

I would amalgamate HighPriotityInUnblockedQueue and HighPriorityHasWork into one invariant as below

\forall c.
[ prio[c]=1 à
   [ queue[c]=/=\emptyset 
     \/
    \exists c’.[c\in Msgs(c’) /\pri[c’]=1 ]
    /\
    Acquired(c) ]  ]```