プログラミングやってるなら
関数(主張)の返り値(証明)に寄与しない無駄なコード(記述)を削除する
とか、
関数(証明)の処理フロー(論理構造)がわかりやすくなるように一部を別の関数(補題)として切り出す
みたいに例えたらわからんかねえ……