At:
not is member remove lemma112
1.
T: Type
2.
eq: {T=}
3.
x: T
4.
y: T
5.
L: T List
6.
eq(x,y)
7.
u: T
8.
v: T List
9.
x(eq) v x(eq) remove(eq;y;v)
10.
if eq(x,u) true else x(eq) v fi
11.
eq(y,u) = false
x(eq) (u.remove(eq;y;v))
By:
AbReduce 0
THEN
IfThenElseCases 0
Generated subgoals:
true
eq) remove(eq;y;v)
eq(x,y)
x(
true
