add axiom_use generator

[digama0]

Based on a request at metamath/set.mm#3150 (comment) . This generates a list of the axioms used by every statement in set.mm, like so:

a1ii:
idi:
mp2: ax-mp
mp2b: ax-mp
a1i: ax-mp ax-1
2a1i: ax-mp ax-1
mp1i: ax-mp ax-1
a2i: ax-mp ax-2
mpd: ax-mp ax-2
...

It takes about 200ms to generate the file.

Some caveats: This is only really designed to work for set.mm. In particular it bakes in two assumptions which are correct for set.mm but not necessarily for other databases:

• It only supports compressed proofs, and will panic on normal mode proofs, and possibly panic or give the wrong result on packed proofs.
• It assumes that axioms are marked with the ax- prefix, meaning that definitions are ignored, but also nonstandardly named axioms.

[tirix]

All good for me, just one point I don't fully understand.