Def zero_rep == @x:. (y:. x = suc_rep(y)  )

is mentioned

In prior sections: hol num

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