--> τ</code>. This looks like logical implication. Let's take
-that resemblance seriously. Then note that types respect modus
-ponens: given two expressions <code>fn:(σ -> τ)</code> and
-<code>arg:σ</code>, the application of `fn` to `arg` has type
-<code>(fn arg):τ</code>.
-
-Here and below, writing <code>x:α</code> means that a term `x`
-is an expression with type <code>α</code>.
-
-This is a special case of a general pattern that falls under the
-umbrella of the Curry-Howard correspondence. We'll discuss
-Curry-Howard in some detail later.
-
-System F is due (independently) to Girard and Reynolds.
-It enhances the simply-typed lambda calculus with quantification over
-types. In System F, you can say things like
+-> τ</code>. This looks like logical implication. We'll take
+that resemblance seriously when we discuss the Curry-Howard
+correspondence. In the meantime, note that types respect modus
+ponens:
+
+<pre>
+Expression Type Implication
+----------------------------------
+fn α -> β α ⊃ β
+arg α α
+------ ------ --------
+fn arg β β
+</pre>
+
+The implication in the right-hand column is modus ponens, of course.
+
+System F is usually attributed to Girard, but was independently
+proposed around the same time by Reynolds. It enhances the
+simply-typed lambda calculus with quantification over types. In
+System F, you can say things like