Fib 2 = Fib ((0 + 1) + 1)
.= 1 by PRE_FF:1 ;
hence Fib 2 = 1 ; :: thesis: verum