At:
hd is member lemma1211121
1.
T: Type
2.
eq: {T}
3.
eq TT
4.
x,y:T. eq(x,y) eq(y,x)
5.
x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
6.
L: T List
7.
u: T
8.
v: T List
9.
||v||1 hd(v)(eq) v
10.
||u.v||1
11.
eq(u,u) = false
12.
eq(u,u)
u(eq) v
By:
HypSubst -2 -1
THEN
Rewrite (HigherC assert_evalC) -1
Generated subgoal:
u(
eq) v
}
T
x,y:T. eq(x,y) 
eq(y,x)
1 
