At: mem select 1 2 1 1 1
1. T: Type
2. L: T*
3. t: T
4. u: T
5. v: T*
6. mem_f(T;t;v) 
(
i:
||v||. v[i] = t)
7. mem_f(T;t;v)
8. i: ||v||
9. v[i] = t
10. 0 < i+1
hd(nth_tl(i+1-1;tl((u.v)))) = t
By:
Fold `select` 0
THEN
Reduce 0
THEN
ArithSimp 0
Generated subgoals:None
About:
