'a:S. 
  and
  (all(P:'a  hbool. equal(every(P,nil),t))
  ,all
  ,(P:'a  hbool. all
  ,(P:'a  hbool. (h:'a. all
  ,(P:'a  hbool. (h:'a. (t:hlist('a). equal
  ,(P:'a  hbool. (h:'a. (t:hlist('a). (every(P,cons(h,t))
  ,(P:'a  hbool. (h:'a. (t:hlist('a). ,and(P(h),every(P,t)))))))

1	1. 'a : S 2. P : 'a   every(P;nil) = true	1 step
2	1. 'a : S 2. P : 'a 3. h : 'a 4. t : 'a List   every(P;cons(h; t)) = ((P(h))every(P;t))	1 step

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