ve the following law:</p>
<p>If <code>x</code> is a variable, <code>T</code> is a type and <code>U</code> is type in which there is no free occurrence of <code>x</code>, then:</p>
<pre><code class="language-clojure">(forall  [x T] U) ≝ (==&gt; T U)
</code></pre>
<p>(so implication is a special case of universal quantification)</p>
<p>Hence the type of our <em>modus ponens</em> example becomes:</p>
<pre><code class="language-clojure">(forall [A :type]
  (forall [B :type]
    (==&gt; A
         (==&gt; (==&