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