    x))
</code></pre>
<p>However, in practice, the references for theorems are not unfolded because it is useless since we already know the type of the proof term. Otherwise, the proofs that reference many theorems would yield very large proof terms.</p>
<h3><a href="#fundamental-properties" id="fundamental-properties"></a>Fundamental properties</h3>
<p>We now discuss the fundamental properties of the calculus of constructions with definitions that is implemented in LaTTe. These properties are important req