I am reading about embedding/automation of modal logics in classical higher order logic (http://page.mi.fu-berlin.de/cbenzmueller/papers/C46.pdf) and Goedels proof of God’s existence is prominent example here https://www.isa-afp.org/entries/GoedelGod.html (as encoded for Isabelle/HOL).

This embedding has embedding for Leibniz equality for individuals:

`abbreviation mLeibeq :: "μ ⇒ μ ⇒ σ" (infixr "mL=" 90) where "x mL= y ≡ ∀(λφ. (φ x m→ φ y))" `

and this type of euqality is used for the first axiom already:

`A1a: "[∀(λΦ. P (λx. m¬ (Φ x)) m→ m¬ (P Φ))]" `

which can be written without lambdas as:

`A1a: ∀φ[P(¬φ)↔¬P(φ)] `

My question is – how to understand the expression `∀(λφ. (φ x m→ φ y))`

, because usually we have `∀x.P(x)`

? I.e. universal quantifier expects the argument (`x`

) and the predicate (`P(x)`

), but this expression contains noone know what? is entire `(λφ. (φ x m→ φ y))`

and argument `x`

or Predicate `P(x)`

? What can be omitted here, what is the convention used here?