Add a "statement use" option

[tirix]

As suggested by @GinoGiotto in a comment in #3399, this adds an option to get direct of indirect usage of theorems, given by the list of their labels.

[GinoGiotto]

That's very nice! Definitely I'll apply it for axiom minimizations (this is useful as well for activities like https://github.com/metamath/set.mm/pull/3431, because I needed to list all theorems using df-clel but not ax-8, and --axiom-use doesn't tell definitions, so it wasn't enough for that).

Thank you so much for this work!

[GinoGiotto]

I executed the command cargo run -- set.mm --stmt-use nfmo,nfmod,nfmod2 and it works, but it prints the output directly on the command line. Can the output be printed in a text file like --axiom-use does?

[tirix]

It works, but it prints the output directly on the command line.

Yes, that's not ideal. How about changing the parameters so that --stmt-use would take two parameters, the file name and the list of labels, like this:

OPTIONS:
    -X, --axiom-use <FILE>            Generate `axiom-use` file
        --stmt-use <FILE> <LABELS>    Outputs statements directly or indirectly using the given list of statements

[GinoGiotto]

Sounds good, I like it.

[tirix]

I've committed an update which does that.

I could not use the validator function because it would be applied both on the file path and the label list, so I moved it into our own code.