"彼ら"に証明させるとあまりgrindを使ってくれなくて言わないと使ってくれないが、逆に使わせすぎるとコードに顕れる議論が少なくなって良くないのかもしれない（人間側に「自明」と書かれた形式証明だけ寄越されても困る）

@SnO2WMaN これは自明なことかもしれませんが、grind onlyを義務付けるとかが落とし所なのかなと思います。

@dec9ue そうなると逆に保守性に欠ける（当該補題が消えたりリネームされたらその部分もリファクタリングする必要がある）ので難しいところではあります．

@SnO2WMaN ごもっともで、いい塩梅の書き方があるといいんですが 欲しいのは「大体こういうことした」的な情報というか 一例として使った補題だと思うのですが、これも粒度がマチマチというか