Generate more concise identifiers for the Lean 4 definition

[tothtamas28]

Munged KORE identifiers tend to be very long. The current implementation only replaces - by _ to obtain a valid Lean identifier.

Instead, we could do the following:

• Drop the Lbl prefix (if any), then unmunge. If it is a valid Lean 4 identifier, done.
• Otherwise, surround it by « and ».

Note that since Lbl is dropped from the symbol identifier, the Sort prefix has to be preserved in sort identifiers to avoid collision.