is mentioned by

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]
Thm* a,b,c:T List. l_disjoint(T;c;a @ b) l_disjoint(T;c;a) & l_disjoint(T;c;b)	[l_disjoint_append2]
Thm* a,b,c:T List. l_disjoint(T;a @ b;c) l_disjoint(T;a;c) & l_disjoint(T;b;c)	[l_disjoint_append]
Thm* a,b:T List, t:T. l_disjoint(T;b;[t / a]) (t b) & l_disjoint(T;b;a)	[l_disjoint_cons2]
Thm* a,b:T List, t:T. l_disjoint(T;[t / a];b) (t b) & l_disjoint(T;a;b)	[l_disjoint_cons]

Try larger context: Graphs