ИМХО, это проблема больше синтаксическая, если идея решения уже зафиксирована, то остается только упрощать сам текст, руководствуяюсь в основном формальными требованиями к синтаксису. (опять же ИМХО, много похожих требований есть в руководствах к правильному написанию программного кода, но для этого нужна хоть какая-то специализация. Прежде всего это принцип DRY
https://ru.wikipedia.org/wiki/Don%E2%80 ... t_yourself).
Можно попытаться какие-то приемы изложить, но их будет много и они не всегда будут четкие:
1. Если терм встречается несколько раз - нужно назвать его какой-нибудь буквой и рассуждать о нем.
2. Если рассуждение встречается несколько раз - его надо выделить в отдельную лемму.
3. Если часть рассуждения использует другой инструментарий или просто некие временные переменные - его надо оформить отдельно в лемму или хотя бы в абзац.
4. Каждое рассуждение должно быть простым и иметь форму логической тавтологии (закон исключенного третьего, контрапозиция и т.п.)
5. Если часть рассуждения не используется - его следует убрать.
6. Бывает так, что временная переменная (подстановка) используется несущественно - о ее свойствах нет никаких рассуждений - такую переменную следует заменить на ее выражение (это против 1, просто используется в своих случаях).
7. Если часть рассуждения общеизвестна - лучше на него сослаться (как на библиотеку)
И т.п. Можно продолжать дальше.
Если доказательство плохо укладывается в эту схему, значит с ним все плохо (
быдлокод) - его надо разбивать на куски и разбираться с каждым куском отдельно.