Nuprl - Proof: card boolset vs mset 1 2 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. 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) = k

By:	Rewrite by Hyp:5

Generated subgoal:

1 Msize(x.if f(x)=1 1 else 0 fi) = Msize(f)
1 step

About:

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