'a,'b:S.
  all
  (P:'a  hbool. all
  (P:'a  hbool. (B:'a  'b. equal
  (P:'a  hbool. (B:'a  'b. (res_abstract(P,B)
  (P:'a  hbool. (B:'a  'b. ,x:'a. cond(P(x),B(x),arb))))

1

1. 'a : S 2. 'b : S 3. P : 'a 4. B : 'a'b   res_lambda('a;'b;x.P(x);x.B(x)) = (x:'a. if P(x) then B(x) else arb('b) fi )

1 step

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