ill see how to distinguish them.</p>
<p>A (low-level) lambda-term in LaTTe is either:</p>
<ul>
<li>the constant: <code>✳</code> named <strong>type</strong></li>
</ul>
<p>This corresponds to the <em>type of types</em>. A lambda-term is said a <em>proper type</em> if its type is <code>□</code>. In the concrete syntax <code>□</code> is more conveniently written <code>:type</code>.</p>
<ul>
<li>the constant  <code>□</code> named <strong>kind</strong></li>
</ul>
<p>This is to give a type to <code>□</co