and
  (all(m:hnum. equal(exp(m,0),1))
  ,all(m:hnum. all(n:hnum. equal(exp(m,suc(n)),mult(m,exp(m,n))))))

1

1. m :  2. n :    exp(m;n+1) = mexp(m;n)

2 steps

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