Nuprl - Proof: hexp wd 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hexp wd 1

1. m :

2. n :

exp(m;n+1) = m

exp(m;n)

By:	Assert (n+1>0) THEN Simp THEN Try (Complete Auto)

Generated subgoal:

1 3. n+1>0
mexp(m;n+1-1) = mexp(m;n)
1 step

About:

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