as:T*, i:{0...||as||}, j:{i...||as||}, k:{j...||as||}.
((as[i..j
]) @ (as[j..k])) = (as[i..k])
append_segment
bs ; a.as' a.(as' @ bs) (recursive)
Thm* as:T*, i:{0...||as||}, j:{i...||as||}, k:{j...||as||}.
((as[i..j]) @ (as[j..k])) = (as[i..k])
append_segment
Thm* x:
, as:T*. x < ||as|| 
firstn(x+1;as) = (firstn(x;as) @ [as[x]])
firstn_lem1
Thm* L1,L2:T*, t:T. mem_f(T;t;L1 @ L2) 
mem_f(T;t;L1) 
mem_f(T;t;L2)
mem_append
In prior sections: list 1