At:
sublist tail
1
1
1
1
1
1
1
1
1
1.
T: Type
2.
Discrete{T}
3.
eq: {T
}
4.
eq 
T
T
5.
u: T
6.
v: T List
7.
f1: {T=}
8.
x,y:T. f1(x,y) 
eq(x,y)
9.
xv.if eq(x,u)
true else x(eq) v fi 
(z:T. z(f1) v if eq(z,u) true else z(eq) v fi)
10.
z: T
11.
z(f1) v
12.
eq(z,u) = true
true
By:
Rewrite (HigherC assert_evalC) 0
THEN
Trivial
Generated subgoals:
None
About:
