Nuprl - Proof: card boolset vs mset 1 1 1

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

1. a :

2. k :

3. p :

size(

a)(p) = k

Msize(

i.if p(i)

1 else 0 fi) = k

By:	(-1) Def of size(a) THEN Reduce Hyp:-1

Generated subgoals:

None

About:

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