Nuprl - Proof: card st sized bool 1

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

1. k :

2. a :

3. p :

size(

a)(p) = k

{i:

a| p(i) } ~

By:	Rewrite by Thm* p:(a). {x:a\| p(x) } ~ (size(a)(p))

Generated subgoal:

1 (size(a)(p)) ~ k
1 step

About:

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