At:
non nil is member
1
2
1
1
1.
T: Type
2.
eq: {T
}
3.
eq 
T
T
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 
nil (
x:T. x(eq) v)
10.
u.v nil
11.
eq(u,u)
12.
eq(u,u) = true
u(eq) (u.v)
By:
Rewrite (HigherC is_member_unrollC) 0
THEN
HypSubst 12 0
THEN
Rewrite (HigherC ifthenelse_evalC THENC assert_evalC) 0
Generated subgoal:
| 1 | True |
About:
