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, ...