>>921

>この結果は Lean3 のものです。
Lean4 では型理論が拡張されており（入れ子の帰納型、構造体に対する 規則など） Carneiro 自身が後の論文で「2019年の健全性証明はもはや直接には適用できない」と述べています