 Before moving on to the model theory for \(\LKe\), we pause to note a few features of the deductive system. To illustrate the level of rigor, we begin with a lemma that if a sentence does not contain a particular closed term, we can make small changes to the set of sentences we prove it from without problems. We allow ourselves the liberty here of extending some previous notation: for any terms \(t\) and \(t'\), and any formula \(\theta\), we say that \(\theta(t|t')\) is the result of replacing all free occurrences of \(t\) in \(\theta\) with \(t'\).