iterateP : (a → a) → a → List(a)
iterateP f p = p :: iterateP f (f p)

fib2_helper : ℕ×ℕ → ℕ×ℕ
fib2_helper (a,b) = (b,a+b)

indexP : ℕ -> List(a) -> a
indexP 0 (p::_) = p
indexP (n+1) (_::l') = indexP n l'

fib2 : ℕ → ℕ
fib2 n = {? x when (indexP n (iterateP fib2_helper (0,1))) is (x,_) ?}