1. n : 
2. k:. k<n  (x,y:. fib(k)x+fib(k+1)y = 1)
3. n+1 = 1
  a,b:. fib(n-1)b+fib(n)(a+b) = 1

By:	Inst: Hyp:2 Using:[n-1] THEN Subst-1: n-1+1 = n

1

4. x,y:. fib(n-1)x+fib(n)y = 1   a,b:. fib(n-1)b+fib(n)(a+b) = 1

2 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html