At: select mem 1 2
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)
7. 0 < i
u = hd(nth_tl(i-1;v)) 
mem_f(T;hd(nth_tl(i-1;v));v)
By:
Fold `select` 0
THEN
Sel 2 (Analyze 0)
THEN
BackThru 5
Generated subgoals:None
About:
