寒い。起床は8時半、出勤してコード書き。忘年会の幹事を仰せつかる。また、研究班配属がやっと正式に発令し、辞令を受け取る（3月までの任務だけど）。 Agdaの方は、Non-terminateはsubstitutionと量化子がごちゃごちゃになっているせいだと判断し、両者を…