eq:{T
}, L,M:T List. disjoint(eq;L;M) 
disjoint(eq;L;M)(eq;L;M) == (letrec disjoint2 L = (Case of L; nil 
true ; h.t if h(
eq) M false else disjoint2(t) fi) ) (L)
is mentioned by
| Thm* eq:{T}, L,M:T List. disjoint(eq;L;M) disjoint(eq;L;M) | [disjoint_iff_assert_disjoint2] |