 As is typical in other subjects where the concepts appear, such as first-order logic, one needs to be careful about the issue; a casual attitude about substitution can lead to syntactic  difficulties.[1]  We can defend a casual attitude by adopting the convention that we are interested not in terms themselves, but in a certain equivalence class of terms. We now define substitution, and then lay down a convention that allows us to avoid such difficulties.