Correctly show inferred parameter type in lambda example

[dijkstracula]

In "Function Abstraction and Evaluation", the examples of function abstractions where the Nat argument is documented as being inferred are in fact not: λ x: Nat => x + 5 still annotates the type of x! This patch simply corrects the example to let the type inference engine infer the type.

Additionally, this section was missing a few pieces (later on, functions are bound to names using def but this special form is never explicitly called out; exactly when may function types' return types be annotated), so I attempted to succinctly fill in a few of those gaps.