At:
remove is member lemma
1
1
1
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) = true
14.
v(eq) v1
15.
eq(v,u1) = true
true
By:
Rewrite assert_evalC 0
THEN
Trivial
Generated subgoals:
None
About:
