At:
is member remove lemma1221
1.
T: Type
2.
eq: {T=}
3.
eq TT
4.
x,y:T. eq(x,y) x = y
5.
L: T List
6.
x: T
7.
u: T
8.
v: T List
9.
eq(x,u) = false
10.
xx: x(eq) v
11.
M: T List
12.
N: T List
13.
v = (M @ (x.N)) & remove(eq;x;v) = (M @ N)
M,N:T List. u.v = (M @ (x.N)) & u.remove(eq;x;v) = (M @ N)
By:
Witness u.M
THEN
Witness N
THEN
Reduce 0
Generated subgoal:
u.v = u.(M @ (x.N)) & u.remove(eq;x;v) = u.(M @ N)
}
T
T
x,y:T. eq(x,y) 
x = y
M,N:T List. u.v = (M @ (x.N)) & u.remove(eq;x;v) = (M @ N)
