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: Aug 23 2025 at 01:39 UTC