Nuprl - graph_1_1 LEMMAs for no_repeats_append

Rank	Theorem	Name
2	Thm* l1,l2:T List. no_repeats(T;l1 @ l2) l_disjoint(T;l1;l2) & no_repeats(T;l1) & no_repeats(T;l2)	[no_repeats_append_iff]
cites
1	Thm* as,bs:T List, i:{\|\|as\|\|..(\|\|as\|\|+\|\|bs\|\|)}. (as @ bs)[i] = bs[(i-\|\|as\|\|)]	[select_append_back]
1	Thm* as,bs:T List, i:\|\|as\|\|. (as @ bs)[i] = as[i]	[select_append_front]
0	Thm* as,bs:T List. \|\|as @ bs\|\| = \|\|as\|\|+\|\|bs\|\|	[length_append]