'a:S. 
  all
  (P:'a  hbool. all
  (P:'a  hbool. (B:'a  hbool. equal
  (P:'a  hbool. (B:'a  hbool. (res_exists(P,B)
  (P:'a  hbool. (B:'a  hbool. ,exists(x:'a. and(P(x),B(x))))))

1

1. 'a : S 2. P : 'a 3. B : 'a   (res_exists('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