A

The same identifier can be overloaded to name two different constants, that is, two constants with different sorts. A <simpleId> can also be used to name a variable and a constant, provided the variable does not have the same sort as the constant.

When LP formulates hypotheses for use in proving subgoals in a proof, it
generally replaces all free variables in the hypotheses by constants. LP
creates identifiers for these constants by appending the letter `c` and, if
necessary, further digits to obtain an identifier that is not already in use.
Thus LP may replace the variable `x` by the constants `xc`, `xc1`, ...