At:
is member of append lemma11212
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 @ M) x(eq) v x(eq) M
9.
if eq(x,u) true else x(eq) (v @ M) fi
10.
eq(x,u) = false
x(eq) v x(eq) M
By:
HypSubst -1 -2
THEN
Reduce -2
Generated subgoal:
eq) (v @ M)
x(
x(
x(
true
