A good way to look at it is not as two different symbols, but as the difference between a definition and a theorem. So if you are creating a new variable, funct

A good way to look at it is not as two different symbols, but as the difference between a definition and a theorem. So if you are creating a new variable, function, etc. for convenience you assert "x = 5" (or something similar). Since you have no other constraints this variable has to satisfy, this is totally safe. However, if "x" already shows up in one of your formulas you need to be careful because you can't merely assert it is equal to whatever you want.