これまで誤解していたが、Agda2のdata typeの型の定義で、 (n : Nat) -> TermSeq n -> Set みたいな定義はよくて（ちなみに TermSeq nは長さがnのTermの列）、 (n : Nat) -> Term -> Pred (n-1) （ただし Pred 0 = Set） みたいな定義は不可能だ ということ…

起床は9時、少し遅め。出勤してコード書き。この件で時間を取られ、メールを書いたりしなければならなかったのに結局何もできず。気がついたら20時、慌てて退所（帰宅は22時）。Cも東京から帰ってきた。