At: least exists2

  P:{P:(Prop)| i:. P(i) }. 
  (i:. Dec(P(i)))  ({i:| P(i) & (j:. j<i  P(j)) })

1

1. P : Prop 2. i:. P(i)  [not for witness] 3. i:. Dec(P(i))   {i:| P(i) & (j:. j<i  P(j)) }

8 steps

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