Nu

和 nu 有關的性質總是證不出來。覺得可能是因為用 lambda 做 modelling 太強了，之前忽略的條件 name occurrences 似乎也對情勢沒什麼影響。又卡住了…

--
趁機跳回 graphical games 一陣子？XD

---

看起來是 "name" type 的問題。Coq paper 裡面直接預設一些關於 name type 的性質（as Axioms），而我們的 encoding 裡面 name type 是任意的 a : Set，直覺上的確性質比較少。

摘錄一句（from p.~22）：These properties capture the idea that functions of type name->proc are actually "processes with a hole", which can be filled in by any name without changing the structure of the process itself.

--
可是隨便 postulate 好像有危險…