>>683 補足

まあ、新一さんは 『[EssLgc]​§1.12でも指摘』をあげていて
「なんか誤解している人がいるが、IUTは自明」だ
と思っていた
ところが、>>661 "３つの不定性 Ind1, Ind2, and Ind3 や 用語“blurring”に関連する概念が
いかにも自然言語であって そこが厳密なLean語に翻訳できない原因かもしれない・・"
となって いまここ

まあ、新一さん含めて 研究室の人たちの頑張りどころですね （＾＾