[Lean] Ensure that generated spec lemmas are communicated to mvcgen #1818
Description
Currently, we mark the generated Spec-definitions with @[spec], but this is not enough to make mvcgen aware of them. We can probably override the @[spec] attribute to extend its behavior.