Improve readability of global invariants

[sim642]

Currently global unknowns have very lengthy names like "longjmp:DeadBranch:MCP.V:base:priv:protected:g:protected" because every Spec functor which wants to add its own global unknowns lifts the inner ones, adding a lifting level to the prefix. This PR removes the variant prefix from unknowns that are lifted from the inner analysis (the ones added still get a prefix as if they were normal analyses). So this turns into "base:priv:protected:g".

The same is also done to the lifted global domain, to remove the excessive "Lifted1" wrappers which are there just for technical reasons and add nothing.

Before

After