(19steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nat to nat pair surj
  Surj(; ; nat_to_nat_pair)
By: Def

Generated subgoal:

1   b:(). a:. nat_to_nat_pair(a) = b
18 steps

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

(19steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc