Naturally, you cannot tell in advance what other people would use from your proof development, but what is a good workflow for this?
You could set up simplification rules from good lemmas, make the main definitions and theorems, induction rules visible. What else?
Last updated: Sep 13 2025 at 12:36 UTC