|
|
|
|
|
|
by mayoff
829 days ago
|
|
|
The fib' function (the more efficient version of fib) is defined using f. So the goal is to prove that f computes the same thing as fib (given the appropriate arguments to f and fib). Hence the theorem needs to use f on at least one side of the equation. |
|
|