'a:S. 
  all
  (P:'a  hbool. all
  (P:'a  hbool. (B:'a  hbool. equal
  (P:'a  hbool. (B:'a  hbool. (res_forall(P,B)
  (P:'a  hbool. (B:'a  hbool. ,all(x:'a. implies(P(x),B(x))))))

1

1. 'a : S 2. P : 'a 3. B : 'a   (res_all('a;x.P(x);x.B(x))) = (x:'a. (P(x))(B(x)))

1 step

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