At:
not disjoint is member lemma111211111111
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
u(eq) M
By:
Assert Stable{u(eq) M}
Generated subgoals:
Stable{u(
eq) M}
}
T
x,y:T. eq(x,y) 
x = y
disjoint(eq;v;M) 
x:T. x(
