(11steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card pi vs nsub pi 1 1

1. b : 0
  (i:0b(i)) ~ 1


By: BackThru: Thm*  (A ~ 1)  (!A)


Generated subgoal:

1   !(i:0b(i))
2 steps

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

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