-because the first argument `s` must apply to the second argument `z`,
-the type of the first argument must describe a function from
-expressions of type σ to some other type. So we can refine ρ
-by replacing it with the more specific type σ --> τ. At
-this point, the overall type is (σ --> τ) --> σ -->
+because the first argument (`s`) must apply to the second argument
+(`z`), the type of the first argument must describe a function from
+expressions of type σ to some result type. So we can refine
+ρ by replacing it with the more specific type σ --> τ.
+At this point, the overall type is (σ --> τ) --> σ -->