Universal Elimination:

Here for any sentence, there is A, containing a universally quantified variable, v, just for any ground term, g, so we can substitute g for v in A. Thus we write the following to represent this rule:

  ∀v A/Subst({v/g}, A)

As show an example from Russell and Norvig that a rule can be used on the following sentence: as ∀X, likes(X, ice_cream) to substitute the variable 'ben' for X, for giving us the sentence as ben, ice_cream. In generally English, this might says that there given everyone like ice cream, so we can infer here that Ben likes ice cream. Thus this is not exactly rocket science and  just  for that it is worth bearing in mind beneath all the fancy symbols in logic, so we're really only saying simple things.