At:
is member append lemma121111111
1.
T: Type
2.
eq: {T=}
3.
eq TT
4.
x,y:T. eq(x,y) x = y
5.
L: T List
6.
x: T
7.
u: T
8.
v: T List
9.
x(eq) v (M,N:T List. v = (M @ (x.N)))
10.
eq(x,u) = true
eq(x,u)
By:
HypSubst -1 0
THEN
Reduce 0
Generated subgoals:
}
T
T
x,y:T. eq(x,y) 
x = y
M,N:T List. v = (M @ (x.N)))
eq(x,u)
