Nuprl - Proof: card st vs msize 1 1 1

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

1. a :

2. P :

Prop
3. f :

2
4.

a. P(i)

f(i) = 1
5. x : {x:

a| P(x) }

(f(x))

By:

Analyze-1

Generated subgoal:

1 5. x : a
6. P(x)
0 (f(x))
1 step

About:

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