An attempt to translate the formalization of Gödels Incompleteness Theorem from Coq to Arend based on this: https://r6.ca/Goedel/goedel1.html
The Coq version: https://github.com/coq-community/goedel And a more up-to-date version: https://github.com/coq-community/hydra-battles/tree/master/theories/goedel