M:T List. 
disjoint(eq;nil;M) 
(
x:T. x(
eq) nil & x(eq) M)7. v: T List
8.
M:T List. disjoint(eq;v;M) (x:T. x(eq) v & x(eq) M) M:T List. disjoint(eq;(u.v);M) (x:T. x(eq) (u.v) & x(eq) M)
}
T
T
x,y:T. eq(x,y) 
x = y
M:T List. disjoint(eq;L;M) (x:T. x(eq) L & x(eq) M)
| 1 | M:T List. disjoint(eq;nil;M) (x:T. x(eq) nil & x(eq) M) |
| 2 | 6. u: T 7. v: T List 8. M:T List. disjoint(eq;v;M) (x:T. x(eq) v & x(eq) M) M:T List. disjoint(eq;(u.v);M) (x:T. x(eq) (u.v) & x(eq) M) |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |
 |