(define f (lambda (n) (if (= n 0) 0 (+ 2 (f ( n 1))))))
The proof  Comments on the proof 

Theorem:For any integer n that is greater
than or equal to 0, (f n)
evaluates to 2n.

The mathematical expression 2n should be thought of as the
name for some specific number, depending on which specific number
n is. The theorem is just a short hand for an
infinitely long list of claims: that (f 0) evaluates to
0, that (f 1) evaluates to 2, that (f 2)
evaluates to 4, etc.

Base case (n = 0): From the code, we see that (f
0) evaluates to 0. Since 0 = 2 × 0, the theorem holds in this
case.
 The base case of the proof verifies that the base case of the code works, and provides a foundation for the induction. We look at the code to see what it does compute, at the theorem to see what it should compute, and use a little math to show that they are equal. In the base case, this is frequently trivial, as here: the code directly tells us what is computed, and the math needed to show equality is just arithmetic. 
Induction hypothesis:
For any integer k that is greater
than or equal to 0 and less than n, (f k)
evaluates to 2k.

This is just a copy of the theorem, but with the variable n
renamed to k and the additional restriction that
k<n. If there were multiple variables in the
theorem, they would each be renamed to a new one, and whichever
variable is the one that decreases towards the base case would be the
one we restrict.
Notice that there are two separate restrictions on k. It must be greater than or equal to 0, and it must be less than n. These come from two different sources. The first is copied along with the rest of the theorem. The second is added to ensure that we only rely on smaller cases in our inductive reasoning. Often times (as in the book) we combine these two into a single statement, that k must be in the range from 0 up to (but not including) n. However, don't let that throw you: there are still two different restrictions, coming from two different sources.
One way to understand why we can safely rely on correct operation for
all values smaller than n while trying to prove correctness
for n is to realize that if the procedure fails for any
argument value, there must be a smallest one that it fails for. We
are showing that whatever value you choose for n, it can't
be the smallest value where 
Inductive step (n > 0):
Because we are now only considering the case that n is
greater than 0, we know it isn't equal to 0, and can see from
the code that the result will be two more than whatever (f ( n
1)) computes. Because n is greater than 0, we know
that n  1 must be greater than or equal to 0. And clearly
n  1 < n. Therefore, we can apply the
induction hypothesis, substituting n  1 for k.
This tells us that (f ( n 1)) evaluates to
2(n  1). This is what 2 then gets added to, producing the
sum 2 + 2(n  1). A little algebra shows that is equal to
2n, so the procedure produces the correct answer in this
case too.

Notice that we restrict our attention to n > 0, because
the base case has already handled the possibility that n =
0. Just like in the base case, we are again figuring out what the
procedure does compute and comparing that with what it
should compute. This time it is a bit less straightforward,
however, to figure out what the procedure computes, and also to check
for equality with what it should compute.
To figure out what the procedure does compute, we need to rely on the
induction hypothesis. Notice that we first verify that the argument
value (which here is n  1) lies in the range where the
induction hypothesis applies. Having done so, we can substitute the
argument value, n  1, in
place of the induction hypothesis's placeholder variable, k.
If you want to think of a concrete example, suppose we look at the
case where n = 10. We see that
To check that the computed value, 2 + 2(n  1), is equal to
the desired value, 2n, requires a little algebra, but
nothing fancy. (Sometimes a bit more is needed, as for the book's
example of 
Conclusion: By mathematical induction,
(f n)
evaluates to 2n, for any integer n that is greater
than or equal to 0.
 This just restates the theorem, pointing out that its truth follows from the above base case and inductive step by the principle of mathematical induction. 
Instructor: Max Hailperin