'a:S. 
  and
  (equal(null(nil),t)
  ,all(t:hlist('a). all(h:'a. equal(null(cons(h,t)),f))))

1

1. 'a : S 2. 'a List 3. 'a   False

1 step

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