eq:{T=
}, L,M:T List. 
disjoint(eq;L;M) 
(
x:T. x(
eq) L & x(eq) M)p:
. p 
p Dec(Q) ((P & Q) P 
Q)| Theorem | Name | ||
| Thm* eq:{T=}, L,M:T List. disjoint(eq;L;M) (x:T. x(eq) L & x(eq) M) | [not_disjoint_is_member_lemma] | ||
| cites | |||
| Thm* p:. p p | [assert_of_bnot] | ||
| Thm* Dec(P) Dec(Q) ((P & Q) P Q) | [demorgan2] |