早安

又到五點了 XD。要不是卡住，我就可以連續工作十二小時把整個 derivation 寫出來了。真不甘心 XD。

scm 老師論文改第二遍，引言就變得好有感情耶。（絕對沒騙人也不是諂媚，等釋出看了就知道 XD。）而且寫出來的 code 都好漂亮，不像我的都是一團亂碼 XD。（像這次又生產了約一百行亂碼 XD。）這就是功力啊！

--
今天宋明理學剛好停課 XD。

---

如果這樣推導可以嗎？

其中 pf⁺ 把一個 list 映射到它自己和排序證明的 dependent pair，所以再裝上 proj₁ 就會包含在 idR 裡面；加下標 pf 的 insert 和 nil 所處理的 lists 都用 dependent pairs 裝上 sortedness proofs。我沒檢查第二次 fusion 的條件，不過直覺猜它會對 XD。

--
我發現我不太行了，還是去睡吧 XD。

---

乾脆再把 proj₁ 也融進 foldr 裡面嘛！這樣就把證明全消掉了！

身體有點累，但精神亢奮中 XD。

--
七點了，要直接吃早餐了嗎？XD