Nuprl - Proof: card st vs msize 1 1 2

(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 2

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 : i:

a

(f(i))
7. x :

a
8. i :

(f(x))
9. xi = <x,i>

x

{x:

a| P(x) }

By:

Analyze

Generated subgoal:

1 P(x)
1 step

About:

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

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