  In recent years, G\"odel's ontological proof and variations of it were
formalized and analyzed with automated tools in various ways. We supplement
these analyses with a modeling in an automated environment based on first-order
logic extended by predicate quantification. Formula macros are used to
structure complex formulas and tasks. The analysis is presented as a generated
type-set document where informal explanations are interspersed with
pretty-printed formulas and outputs of reasoners for first-order theorem
proving and second-order quantifier elimination. Previously unnoticed or
obscured aspects and details of G\"odel's proof become apparent. Practical
application possibilities of second-order quantifier elimination are shown and
the encountered elimination tasks may serve as benchmarks.
