てか望月先生の論文によれば基礎の公理を排除したZFC上ならiutは通常の推論則上で成立するらしい。ならleanで検証できるからやってみたらいい。
全部打ち込んでちゃんと動けばiutの救済者として歴史に名を残す。失敗してもiut論文の間違い発見者で1000万もらえるらしいからやってみればいい