Thm* as:T*. (as[0..||as||]) = as whole_segment

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* as:T*. firstn(||as||;as) = as firstn_lem0

Thm* L,La:T*. Fin(T) (La':T*. (t:T. mem_f(T;t;La) mem_f(T;t;L) mem_f(T;t;La')) & (t:T. mem_f(T;t;La') mem_f(T;t;La)) & (||La'||1 mem_f(T;hd(La');L))) shorten_list

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

Thm* L:T*. ||L||1 mem_f(T;hd(L);L) hd_mem

Thm* L:T*. 0 < ||L|| L = hd(L).tl(L) hd_tl

Thm* L:T*. ||L||0 L = nil zero_nil

In prior sections: list 1 finite sets