(9steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The finite sequences of natural numbers can be placed in one-one correspondence with the natural numbers themselves.

At: card nat vs nat tuples all

  (k:k) ~ 
By: Rewrite after
Inst: Thm: card split sigma dom decbl
Using:[A:=  | B(k):= k | P(k):= 0 = k  ]

Generated subgoal:

1   ((k:{k:| 0 = k   }k)+(k:{k:| 0 = k   }k)) ~ 
8 steps

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

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