Note: the lazy semantics for cons are reflected by three changes to our 
      evaluation rules:
      (i) cons(M,N) is a value for all expressions M,N.
      (ii) first(cons(M,N)) = M 
      (iii) rest(cons(M,N)) = N

   let or      := map x,y to if x then true else y;
       member  := map x,l to if null?(l) then false
                             else or(x = first(l), member(x, rest(l)));
        zeroes := cons(0, zeros);
   in member (1, zeros)

=> let ... in (map x, l to ...)(1, cons(0, zeroes))     [*]
=> let ... in if null?(cons(0,zeroes)) then false
              else or(1 = first(cons(0,zeroes)), member(1,rest(cons(0,zeroes))))
=> let ... in if false then false
              else or(1 = first(cons(0,zeroes)), member(1,rest(cons(0,zeroes))))
=> let ... in or(1 = first(cons(0,zeroes)), member(1,rest(cons(0,zeroes))))   
=> let ... in (map x,y to ...)(1 = first(cons(0,zeroes)), member(1,rest(cons(0,zeroes))))
=> let ... in (map x,y to ...)(1 = 0, member(1,rest(cons(0,zeroes))))
=> let ... in (map x,y to ...)(false, (map x,l to ...)(1,rest(cons(0,zeroes))))
=> let ... in (map x,y to ...)(false, (map x,l to ...)(1,zeroes))
=> let ... in (map x,y to ...)(false, (map x,l to ...)(1,cons(0,zeroes)))
   which is 
   let ... in (map x,y to ...)(false, [**])
   where [*] above is
   let ... in [**]

We have generated exactly the same reduction subproblem (reducing the phrase [**}
as we had in [*] above.  Hence this computation diverges.