At:
append is member lemma1221111
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.
(M,N:T List. v = (M @ (x.N))) x(eq) v
10.
eq(x,u) = false
11.
M: T List
12.
N: T List
13.
u.v = x.N
M,N:T List. v = (M @ (x.N))
By:
ApFunToHypEquands `X' (Case of X; nil x ; h.t h) T 13
THEN
Reduce -1
Generated subgoal:
M,N:T List. v = (M @ (x.N))
}
T
T
x,y:T. eq(x,y) 
x = y
x ; h.t 
