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