At:
hd is member lemma121111
1.
T: Type
2.
eq: {T}
3.
eq TT
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.
L: T List
8.
u: T
9.
v: T List
10.
||v||1 hd(v)(eq) v
11.
||u.v||1
12.
eq(u,u) = true
true
By:
Rewrite (HigherC assert_evalC) 0
THEN
Trivial
Generated subgoals:
}
T
T
x:T. eq(x,x)
eq(y,x)
1 
true
