 logic.</p>
<p>Moreover, if in <code>(Π [x T] U)</code> the variable <code>x</code> does not occur freely in <code>U</code>, then an equivalent notation is <code>(==&gt; T U)</code>.  This is thus not only universal quantification but <em>also</em> (as a specific case) the type of functions from <code>T</code> to <code>U</code> <em>and</em> the <em>implication</em> that from <code>T</code> we can get <code>U</code>.</p>
<p>A syntactic shortcut allows to chain the implications:</p>
<pre><code class="languag