Nuprl - Proof: card0 iff uninhabited

(8steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Search Doc

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
A class has zero members just when it doesn't have any.

At: card0 iff uninhabited

A:Type. (A ~

(

By:

Auto

Generated subgoals:

1 1. A : Type
2. A ~ 0
(A)
3 steps

2 1. A : Type
2. (A)
A ~ 0
4 steps

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

(8steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Search Doc

1	1. A : Type 2. A ~ 0 (A)	3 steps
2	1. A : Type 2. (A) A ~ 0	4 steps