Proof tree

打 Martin-Löf 的 intuitionistic type theory 講義練習用右手按 shift，打到 bounded μ-operator 的時候有棵龐大的 proof tree。雖然 bussproofs 很好用，對著樹直覺地做 post-order traversal 就打完了，但整棵樹因為太寬立刻超出頁面。和原稿相比較，一些枝葉茂盛的 subtrees 應該延伸到旁邊比較小的 subtrees 上面，但 bussproofs 不會做這種最佳化，\insertBetweenHyps 對於三個前提的 inference 又沒辦法指定特定一個間隔插入 \hskip，於是乾脆直接改 bussproofs 的源碼，才把樹調得窄一點，但還是塞不進 \textwidth。最後只好手動調整，讓樹均勻超過左右邊界 XD。

--
不懂的源碼也照改，這就是資訊系的訓練？XD