Thm* x:, as:T*. x < ||as|| firstn(x+1;as) = (firstn(x;as) @ [as[x]]) firstn_lem1

Thm* L:T*, t:T. mem_f(T;t;L) (i:||L||. L[i] = t) mem_select

Thm* L:T*, i:||L||. mem_f(T;L[i];L) select_mem

In prior sections: list 1