At:
not disjoint is member lemma111211111121
1.
T: Type
2.
eq: {T=}
3.
eq TT
4.
L: T List
5.
u: T
6.
v: T List
7.
M:T List. disjoint(eq;v;M) (x:T. x(eq) v & x(eq) M)
8.
M: T List
9.
u(eq) M
10.
eq(u,u) = false
11.
eq(u,u) u = u
u(eq) v & u(eq) M
By:
HypSubst -2 -1
THEN
Reduce -1
Generated subgoal:
u = u
u(
eq) v & u(
}
T
M:T List. 
disjoint(eq;v;M) 
x:T. x(
