Nuprl - Proof: card st vs msize 1 1 3 1 1

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card st vs msize 1 1 3 1 1

1. a :

2. P :

a

Prop
3. f :

a

2
4.

i:

a. P(i)

f(i) = 1
5. (

x.<x,0>)

{x:

a| P(x) }

(i:

a

(f(i)))
6. (

xi.xi/x,i. x)

(i:

a

(f(i)))

{x:

a| P(x) }
7. i :

a
8. y1 :

(f(i))

<i,0> = <i,y1>

i:

a

(f(i))

By:

Analyze

Generated subgoals:

None

About:

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

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