a,b,c:T List. l_disjoint(T;c;a @ b) 
l_disjoint(T;c;a) & l_disjoint(T;c;b)x:T, l1,l2:T List. (x 
l1 @ l2) (x l1) 
(x l2)| Rank | Theorem | Name |
| 3 | 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] |
| cites | ||
| 2 | Thm* x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2) | [member_append] |