(6steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub bool
   ~ 2
By: Witness: b.if b 1 else 0 fi | i.if i=0 false ; true fi

Generated subgoal:

1   InvFuns(;2;b.if b 1 else 0 fi;i.if i=0 false ; true fi)
5 steps

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

(6steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc