At:
append is member lemma
1
1
1
1
1
1
1.
T: Type
2.
eq: {T=
}
3.
eq 
T
T
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.
nil = x.N
False
By:
ApFunToHypEquands `z' (Case of z; nil 
0 ; h.t 1) 
9
THEN
Reduce -1
Generated subgoals:
None
About:
