Nuprl - Pf select

1. T: Type
2. L: T*
3. u: T
4. v: T*
5. i:||v||. mem_f(T;v[i];v)
6. i: (||v||+1)

u = (u.v)[i] mem_f(T;(u.v)[i];v)

By: Unfold `select` 0 THEN RecUnfold `nth_tl` 0 THEN SplitOnConclITE THEN Reduce 0

Generated subgoals:

1 7. i0
u = u mem_f(T;u;v)

2 7. 0 < i
u = hd(nth_tl(i-1;v)) mem_f(T;hd(nth_tl(i-1;v));v)

About:

1	7. `i0` `u = u mem_f(T;u;v)`
2	7. `0 < i` `u = hd(nth_tl(i-1;v)) mem_f(T;hd(nth_tl(i-1;v));v)`