Add linter for specifications well-supported by progress

[R1kM]

In the Lean backend, the progress tactic performs a lot of work to automate proofs and handle the Aeneas monadic translation.
However, the current tactic also assumes particular shapes for specifications, which might change as the tactic evolves.

To avoid surprises, it would be useful to detect when applying progress whether function specifications have the expected shape. This could for instance be done either by analyzing goals and hypotheses inside progress, by using a custom linter, or possibly by providing custom syntax for program specification that ensures the correct shape.