class="language-clojure">(forall [C :type]
  (==&gt; (==&gt; (&gt; x 3) (&lt;= x 8) C)
       C))
</code></pre>
<p>The type of the reference is the same as the type of the unfolded term.</p>
<p>In the case of an axiom, the reference is considered similar to a constant, except with the parameters replaced by the arguments. The most famous (and sometimes controversed) axiom is probably the law of the <em>excluded middle</em> of classical logic. It is defined as follows in LaTTe (in <a href="null">latte.classi