GenericModel comments on Gödel’s Ontological Proof

[GenericModel]

Not sure how they are? It’s been formalized in lean (which checks types).

EDIT: whoops, Isabelle/​HOL, not Lean