At:
is member of append lemma12212
1.
T: Type
2.
eq: {T}
3.
L: T List
4.
M: T List
5.
x: T
6.
u: T
7.
v: T List
8.
x(eq) v x(eq) M x(eq) (v @ M)
9.
if eq(x,u) true else x(eq) v fi x(eq) M
10.
eq(x,u) = false
x(eq) (v @ M)
By:
HypSubst -1 -2
THEN
Reduce -2
Generated subgoal:
eq) v 
x(
x(
x(
true
