Fibonacci function by strout

module Theorem where
open import Data.Nat
open import Definitions
y : ℕ → ℕ
y(suc(suc n))= y(suc n)+ y n
y n = 1
x : FibFunc y
x 0 = Fib0
x 1 = Fib1
x(suc(suc n))= FibN(x(suc n))(x n)
fib-is-FibFunc = x
fib = y