At:
is member non nil1112
1.
T: Type
2.
eq: {T=}
3.
eq TT
4.
x,y:T. eq(x,y) x = y
5.
u: T
6.
L: T List
7.
u(eq) L
8.
M: T List
9.
N: T List
10.
u1: T
11.
v: T List
12.
L = (v @ (u.N)) (v:T, M:T List. L = v.M)
L = ((u1.v) @ (u.N)) (v:T, M:T List. L = v.M)
By:
Reduce 0
THEN
Analyze 0
Generated subgoal:
v:T, M:T List. L = v.M
}
T
T
x,y:T. eq(x,y) 
x = y
