(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 sigma vs nsub sigma 1 1
1. b : 0
  (i:0b(i)) ~ 0
By: BackThru: Thm*  (A ~ 0)  (A) THEN Analyze

Generated subgoal:

1 2. (i:0b(i))
  False
1 step

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

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