仕事がつまらんので逃避中。https://www.cis.upenn.edu/~bcpierce/sf/current/ 読み始めて三年の月日が経とうというのに、まだ半分もいかない。 ちょっと読んでは分からんので中断し、忘れているので最初からやりなおしとかやってりゃ進まないのは当たり前。…

この一週間くらい手を動かしてた、Software Foundationsの「サブシーケンスという関係は推移的である。」ということの証明が出来た!めっさうれしい。 Inductive subseq : list nat -> list nat -> Prop := | subseq_nil : subseq [] [] | subseq_e : forall …