At:
is member non nil11121
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)
13.
L = u1.(v @ (u.N))
v:T, M:T List. L = v.M
By:
Witness u1
THEN
Witness v @ (u.N)
Generated subgoals:
}
T
T
x,y:T. eq(x,y) 
x = y
v:T, M:T List. L = v.M)
