</p>
<p>If a lambda-term <code>e</code> has type <code>U</code> in the context that <code>x</code> is of type <code>T</code>, then the type of <code>(λ [x T] e)</code> is <code>(Π [x T] U)</code>.</p>
<p>In the concrete syntax, the most common used notations are as follows:</p>
<pre><code class="language-clojure">(forall [x T] U) ≡ (Π [x T] U)

(forall [x1 x2 ... xN T] U)
≡ (Π [x1 T] (Π [x2 T] ... (Π [xN T] e) ... ))
</code></pre>
<p>Yes, of course! This is the <em>universal quantifier</em> of the