Comment by llmzero

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.