Nuprl - graph_1_1 LEMMAs for no_repeats

Rank	Theorem	Name
4	Thm* L:T List. no_repeats(T;rev(L)) no_repeats(T;L)	[no_repeats_reverse]
cites
3	Thm* x:T, L:T List. (x rev(L)) (x L)	[member_reverse]
2	Thm* a,b:T List, t:T. l_disjoint(T;b;[t / a]) (t b) & l_disjoint(T;b;a)	[l_disjoint_cons2]
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]
1	Thm* l:T List, x:T. no_repeats(T;[x / l]) no_repeats(T;l) & (x l)	[no_repeats_cons]