Nuprl - Proof: card boolset vs mset 1 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card boolset vs mset 1 2 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

size(

a)(

i.f(i)=

1) = k

By:	Def of size(a) THEN Reduce Concl

Generated subgoal:

1 Msize(x.if f(x)=1 1 else 0 fi) = k
2 steps

About:

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