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) T:Type, L:T*, i:||L||. mem_f(T;L[i];L)| 1 | 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) |
About:
 |  |  |  |  |  |  |