At:
sublist list all lemma1111
1.
T: Type
2.
EQ: {T=}
3.
EQ TT
4.
x,y:T. EQ(x,y) x = y
5.
eq: {T}
6.
eq TT
7.
x:T. eq(x,x)
8.
x,y:T. eq(x,y) eq(y,x)
9.
x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
10.
L: T List
11.
M: T List
12.
xL.x(eq) M
13.
xL.x(eq) M (z:T. z(EQ) L z(eq) M)
z:T. z(EQ) L z(eq) M
By:
RenameVar `xx' 12
THEN
With xx (Analyze -1)
THEN
Trivial
Generated subgoals:
}
T
T
x,y:T. EQ(x,y) 
x = y
