feat: let_projs tactic, recursively adding projections of hypotheses

[kim-em]

let_projs adds let bindings for all projections of local hypotheses, recursively.

It's probably rarely useful interactively, but may be useful as a preprocessing step for tactics such as solve_by_elim.

[digama0]

I'm inclined to not surface this as a user-facing tactic at all, and just have a MetaM tactic for it. This introduces more API surface area which we have to avoid breaking later, without a compelling use case.

[kim-em]

Good idea. I mostly wrote the syntactical frontend so I could test it. I've moved the syntax into the test file, and added a note that it is not useful otherwise.

[nomeata]

Is there no worry that eagerly adding all projections is going to blow up in some cases, with large or deeply nested structures? Or is this only going to be used in places where the user expects to wait a bit longer (interactive exact? maybe)? Or is this simply a normal approach?

[kim-em]

Is there no worry that eagerly adding all projections is going to blow up in some cases, with large or deeply nested structures? Or is this only going to be used in places where the user expects to wait a bit longer (interactive exact? maybe)? Or is this simply a normal approach?

@joehendrix's suggestion is that when other tactics are using this, if it is a user-called tactic it's okay to do something potentially expensive like this, but tactics called by other tactics should not.