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,s to if null?(s) then false
                             else or(x = first(s), member(x, rest(s)));
        countup := map x to cons(x, countup(1+x));
   in member (1, countup(0))

=> let ... in (map x, s to ...)(1, cons(0, countup(1+0)))
=> let ... in if null?(cons(0,countup(1+0))) then false
              else or(1 = first(cons(0,countup(1+0))), member(1,rest(cons(0,countup(1+0)))))
=> let ... in if false then false
              else or(1 = first(cons(0,countup(1+0))), member(1,rest(cons(0,countup(1+0)))))
=> let ... in or(1 = first(cons(0,countup(1+0))), member(1,rest(cons(0,countup(1+0)))))   
=> let ... in (map x,y to ...)(1 = first(cons(0,countup(1+0))), member(1,rest(cons(0,countup(1+0)))))
=> let ... in (map x,y to ...)(1 = 0, member(1,rest(cons(0,countup(1+0)))))
=> let ... in (map x,y to ...)(false, (map x,s to ...)(1,rest(cons(0,countup(1+0)))))
=> let ... in (map x,y to ...)(false, (map x,s to ...)(1,countup(1+0)))
=> let ... in (map x,y to ...)(false, (map x,s to ...)(1,countup(1)))
=> let ... in (map x,y to ...)(false, (map x,s to ...)(1,cons(1,countup(1+1))))
=> let ... in (map x,y to ...)(false, 
                               if null?(cons(1,countup(1+1))) then false
                               else or(1 = first(cons(1,countup(1+1))), member(1,rest(cons(1,countup(1+1)))))
=> let ... in (map x,y to ...)(false, 
                               if false then false
                               else or(1 = first(cons(1,countup(1+1))), member(1,rest(cons(1,countup(1+1)))))
=> let ... in (map x,y to ...)(false, 
                               or(1 = first(cons(1,countup(1+1))), member(1,rest(cons(1,countup(1+1)))))
=> let ... in (map x,y to ...)(false, 
                               (map x,y to ...)(1 = first(cons(1,countup(1+1))), member(1,rest(cons(1,countup(1+1)))))
=> let ... in (map x,y to ...)(false, 
                               (map x,y to ...)(1 = 1, member(1,rest(cons(1,countup(1+1)))))
=> let ... in (map x,y to ...)(false, 
                               (map x,y to ...)(true, member(1,rest(cons(1,countup(1+1)))))
=> let ... in (map x,y to ...)(false, 
                               (map x,y to ...)(true, 
                                                (map x,s to ...)(1,rest(cons(1,countup(1+1)))))
=> let ... in (map x,y to ...)(false, 
                               (map x,y to ...)(true, 
                                                (map x,s to ...)(1,countup(1+1))))
=> let ... in (map x,y to ...)(false, 
                               (map x,y to ...)(true, 
                                                (map x,s to ...)(1,countup(2))))

=> let ... in (map x,y to ...)(false, 
                               (map x,y to ...)(true, 
                                                (map x,s to ...)(1,cons(2, countup(1+2)))))

which is diverging because the innermost member function application
                                                (map x,s to ...)(1,cons(2, countup(1+2)))))
keeps recurring because it never gets to the end of the s.