dec fibs : list num;
--- fibs <= fs whererec fs == 0::1::map (+) (tail fs||fs);