Comment by measurablefunc

If it doesn't correspond to the original proof then you don't know what it is actually formalizing. It could be a buggy proof of ⊥.