＞レベルが上がれば、無味乾燥に定義定理証明を
＞並べてくれる方が理解しやすいし、ありがたい。
そんなことはない。そういう書き方だと、論理的に正しいことは
followできてもそもそも何故そういう概念を考えたのか
そのmotivationとか、どうやったらその証明のアイディアに
辿り着いたのかとかがほとんど分かりようがない場合がある。

なぜか知らないけどこうやったら論理的にはうまく行っている、
ということしか理解できないのでは機械のproof checkerと変わらん