Make atomic triple mask consistent with regular triples

This inverts the meaning of the mask annotation in atomic triples, to match the one of regular triples: the mask now says which invariants may be used by the callee. This means the "mask weaken" and "invariant open" rules for these triples finally look the way they do on regular triples.

For most actual specs, this changes little: those specs already used masks of the form ⊤∖↑N; they can just write ↑N now and then the statement is syntactically identical to what it was before.

Doing this revealed some deficiencies in how AU/AACC are printed when the masks are a bit more complex, so I also fixed that.

Depends on stdpp!294 (merged)