At:
not is member remove lemma11111111
1.
T: Type
2.
eq: {T=}
3.
x: T
4.
y: T
5.
L: T List
6.
u: T
7.
v: T List
8.
x(eq) v x(eq) remove(eq;y;v)
9.
eq(x,u) = true
10.
true
11.
eq(y,u) = true
12.
eq(y,u)
13.
eq(x,u)
14.
x = u
15.
y = u
x = y
By:
OnHyps [14;15] (i.HypSubst i 0)
Generated subgoals:
}
eq) v 
x(
x = y
i.HypSubst i 0)