At:
remove is member lemma
1
1
1
2
1
2
2
1
1
1
1.
T: Type
2.
eq: {T
}
3.
eq 
T
T
4.
x:T. eq(x,x)
5.
x,y:T. eq(x,y) 
eq(y,x)
6.
x,y,z:T. eq(x,y) 
eq(y,z) eq(x,z)
7.
u: T
8.
L: T List
9.
v: T
10.
u1: T
11.
v1: T List
12.
v(eq) remove(eq;u;v1) v(eq) v1
13.
eq(u,u1) = false
14.
eq(v,u1) = true
15.
true
16.
true = false
v(eq) remove(eq;u;v1)
By:
ApFunToHypEquands `b' if b
0 else 1 fi 
-1
THEN
Rewrite (HigherC ifthenelse_evalC) -1
Generated subgoals:
None
About:
