+ <b>match <em><term></em></b>
+ <p>
+ <u>Examples:</u>
+ <ul class="empty">
+ <li> <tt>\forall x,y:nat.x+y=y+x</tt>
+ (commutativity of natural plus)
+ </li>
+ <li> <tt>\forall x,y,z:R.x*(y+z)=x*y+x*z</tt>
+ (distributivity of real times over real plus)
+ </li>
+ <li> <tt>nat \to nat \to nat</tt>
+ (all binary functions over naturals)
+ </li>
+ </ul>
+ </p>