Nuprl - Proof: card st vs msize 1

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

, P:(

Prop), f:(

2).

(

a. P(i)

f(i) = 1

({x:

a| P(x) } ~ (i:

(f(i))))

By:

Auto

Generated subgoal:

1 1. a :
2. P : aProp
3. f : a2
4. i:a. P(i) f(i) = 1 2
{x:a| P(x) } ~ (i:a(f(i)))
8 steps

About:

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