At:
not disjoint is member lemma1112111121111
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
9.
disjoint(eq;v;M)
10.
x: T
11.
x(eq) v
12.
x(eq) M
if eq(x,u) true else x(eq) v fi & x(eq) M
By:
IfThenElseCases 0
THEN
Reduce 0
Generated subgoals:
}
T
T
x,y:T. eq(x,y) 
x = y
disjoint(eq;v;M)
if eq(x,u)
true
