In page 2, there is the theorem: Theorem ∀n in Nat.f n (fib p) (fib (p+1)) = fib (p+n), I think it should be for all p in Nat (fib p) + (fib (p+1)) = fib(p+2), otherwise there is something mysterious here.
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.