(4steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card void dom fun unit 1

1. A : Type
  (0A) ~ 1


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


Generated subgoal:

1   !(0A)
2 steps

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

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