2. L: T*
3. t: T
4. u: T
5. v: T*
6. mem_f(T;t;v)
(
i:
||v||. v[i] = t)7. u = t
mem_f(T;t;v)
i:(||v||+1). (u.v)[i] = t 
T:Type, L:T*, t:T. mem_f(T;t;L) (i:||L||. L[i] = t)| 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. u = t mem_f(T;t;v) i:(||v||+1). (u.v)[i] = t |
About:
 |  |  |  |  |
 |  |  |  |