It's probably not a good idea to use the same variable for both, also 'x' is not a logical statement so the proof would look more like: ∀x. P(x) P(c) where c

It's probably not a good idea to use the same variable for both, also 'x' is not a logical statement so the proof would look more like: ∀x. P(x) P(c) where c can be anything. This is usually called something like instantation or ∀-elimination. I suppose you could call P(c) a trivial consequence of ∀x. P(x), no matter what c is. The formula P(x) could be something like 'if x is human they are mortal, so something like 'if "Scorates" is human they are mortal" is a trivial consequence, as is 'If "Blue" is human they are mortal".