Given a true statement of the form $$\forall x\, \exists y\, (P(y) \implies S(x))$$ How would I go about instantiating this statement? I know that I can use a universal instantiation to yield $$\, \exists y\, (P(y) \implies S(m))$$ for some arbitrary $m$ in the universe, but is the existential instantiation just as simple as usual, i.e, do I just pick a $n$ for which $P$ holds? This would yield $$P(n) \implies S(m)$$ Is this correct?
Also, is an existential instantiation of this form "linked" to the variable $m$ that I introduced with the universal instantiation? That is, do I think of $m$ as being fixed?