feat: generalize_proofs tactic

[alexjbest]

trafficstars

[alexjbest]

There are still a couple of things to do to please the linters, but I'd be glad to receive feedback on this PR at this stage

[digama0]

There are still some TODO items for this tactic remaining, but I think it's fine to merge now.

• It does not handle hypotheses that depend on binders correctly, it gives a result is not type correct error. (A commented-out test displays this issue.) It should forall-quantify the hypotheses to lift them out of whatever context they appear in.
• It should reuse hypotheses in the context when available rather than introducing a new hypothesis.

bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style