Nuprl - Proof: least exists

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: least exists

, P:{P:(

Prop)|

k. P(i) }.

(

k. Dec(P(i)))

(

{i:

k| P(i) & (

P(j)) })

By:	UnivCD THEN Analyze2

Generated subgoal:

1 1. k :
2. P : kProp
3. i:k. P(i) [not for witness]
4. i:k. Dec(P(i))
{i:k| P(i) & (j:i. P(j)) }
8 steps

About:

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