Expression Type Implication
----------------------------------
fn α -> β α ⊃ β
-arg α α
------- ------ --------
-fn arg β β
+arg α α
+------ ------ --------
+fn arg β β
</pre>
The implication in the right-hand column is modus ponens, of course.