とうとう、型づけ規則の定義ができました。 というわけで、簡単な補題を証明しようとしたところ、string_decがうまく扱えなくて挫折しました。証明したかった補題はTAPLに載っている「Inversion of the typing relation」という補題です。TAPL曰く、Immediat…