At:
append is member lemma111121
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.
M: T List
8.
N: T List
9.
u: T
10.
v: T List
11.
nil = (v @ (x.N)) False
12.
nil = u.(v @ (x.N))
False
By:
ApFunToHypEquands `z' (Case of z; nil 0 ; h.t 1) -1
THEN
Reduce -1
Generated subgoals:
}
T
T
x,y:T. eq(x,y) 
x = y
False
0 ; h.t 
-1
