-If on the other hand, `p` is bound to `\y x. x`, then the two dislayed expressions will be the same. Despite this, they are
-two different lambda expressions, and are not convertible. It's only within the frame of our assumptions about the restricted
-arguments we're thinking of supplying them that they behave exactly the same.
+If on the other hand, `p` is bound to `\y x. x`, then the two displayed expressions will return the same result, namely that function.
+
+Despite this, the two displayed expressions are two different lambda terms, and
+are not convertible. It's only within the frame of our assumptions about the
+restricted arguments we're thinking of supplying them that they behave exactly
+alike.