'a:S. 
  all
  (l1:hlist('a). all
  (l1:hlist('a). (l2:hlist('a). equal
  (l1:hlist('a). (l2:hlist('a). (length(append(l1,l2))
  (l1:hlist('a). (l2:hlist('a). ,add(length(l1),length(l2)))))

None

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