At:
not disjoint is member lemma1112111111112
1.
T: Type
2.
eq: {T=}
3.
eq TT
4.
x,y:T. eq(x,y) x = y
5.
L: T List
6.
u: T
7.
v: T List
8.
M:T List. disjoint(eq;v;M) (x:T. x(eq) v & x(eq) M)
9.
M: T List
10.
u(eq) M
11.
eq(u,u) = true
12.
Stable{u(eq) M}
eq) M 
u(
u(
}
T
x,y:T. eq(x,y) 
x:T. x(
