(9steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card nat vs nat tuples all 1 4 1
1. x : k:{k:| 0 = k }k
  x  k:k
By: 2 Times Analyze1

Generated subgoals:

None

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

(9steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc