[francasso]

You should take this proof as saying: if Lean 4 is consistent then New Foundations is consistent. There is no contradiction of Godel's incompleteness theorem.