At:
remove is member112211
1.
T: Type
2.
eq: {T}
3.
x: T
4.
y: T
5.
L: T List
6.
u: T
7.
v: T List
8.
x(eq) remove(eq;y;v) x(eq) v
9.
eq(y,u) = false
10.
eq(x,u) = true
11.
true
12.
true = false
x(eq) v
By:
ApFunToHypEquands `z' if z 0 else 1 fi -1
THEN
Reduce -1
Generated subgoals:
}
eq) remove(eq;y;v) 
x(
x(
0 else 1 fi 
-1
