■

寒い。起床は8時半、出勤してコード書き。忘年会の幹事を仰せつかる。また、研究班配属がやっと正式に発令し、辞令を受け取る（3月までの任務だけど）。
Agdaの方は、Non-terminateはsubstitutionと量化子がごちゃごちゃになっているせいだと判断し、両者を分離してから、mutualな構成によって両者を互い違いに構成する方向へ改める。おかげでnon-terminationの印も消える。よかった、が、今度はmutualな構成をちゃんと書くという別の難題が。
20時に退所、帰宅は21時半。夕食はマカロニのミートソース和え。