Nuprl - Proof: card boolset vs mset 1 2 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card boolset vs mset 1 2 1 1 1

1. a :

2. k :

3. (

p,i. if p(i)

1 else 0 fi)

(

a {k}

)

a {k}

2
4. f :

2
5. Msize(f) = k

Msize(

x.if f(x)=

1 else 0 fi) = Msize(f)

By:	Analyze THEN FunExtensionality THEN SplitITE Concl

Generated subgoals:

None

About:

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