Nuprl - Proof: card pi vs nsub pi 1 1 1

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

1. b :

(i:

b(i))

By:	Witness: x.x

Generated subgoal:

1 2. y : i:0b(i)
(x.x) = y
1 step

About:

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