Type the Skolemization of "everyone has a mother" (existential under a universal → Skolem function)

Answer

∀X ∃Y mother(X, Y) ⇒ ∀X mother(X, m(X))

The existential Y sits inside the universal X, so Y is replaced by the Skolem function m(X) — "the mother of X" — capturing that the witness depends on X. With no universal in scope it would instead be a Skolem constant.