At:
not is member remove lemma11111
1.
T: Type
2.
eq: {T=}
3.
x: T
4.
y: T
5.
L: T List
6.
eq(x,y)
7.
u: T
8.
v: T List
9.
x(eq) v x(eq) remove(eq;y;v)
10.
eq(x,u) = true
11.
true
12.
eq(y,u) = true
13.
eq(y,u)
14.
eq(x,u)
x(eq) v
By:
OnHyps [14;13]
(i.
FwdThru
Thm*T:Type, eq:{T=}. (x,y:T. eq(x,y) x = y) & eq TT
[i])
Generated subgoal:
x(
eq) v
}
eq(x,y)
x(
i.
FwdThru
Thm* 
T:Type, eq:{T=
T
[i])
