Rule of classical first-order logic. Suppose a result B can be proved from a particular proposition ‘Fa’. And suppose that ‘a’ is not mentioned in any of the premises used in the argument, nor in B itself. Then it is as if ‘a’ is an arbitrary example. In this case the rule allows us to infer B from the weaker premise that (∃x)Fx. Provided that something is F, there is going to be something that could function as a counter, just as ‘a’ does.