a,b:T List, t:T. l_disjoint(T;b;[t / a]) 
(t 
b) & l_disjoint(T;b;a)l:T List, a,x:T. (x [a / l]) x = a 
(x l)| Rank | Theorem | Name |
| 2 | Thm* a,b:T List, t:T. l_disjoint(T;b;[t / a]) (t b) & l_disjoint(T;b;a) | [l_disjoint_cons2] |
| cites | ||
| 1 | Thm* l:T List, a,x:T. (x [a / l]) x = a (x l) | [cons_member] |