At:
sublist transitivity
1
1
1
1
1
1
1
1
1
1
1
1.
T: Type
2.
Discrete{T}
3.
eq: {T
}
4.
eq 
T
T
5.
x:T. eq(x,x)
6.
x,y:T. eq(x,y) 
eq(y,x)
7.
x,y,z:T. eq(x,y) 
eq(y,z) eq(x,z)
8.
L1: T List
9.
L2: T List
10.
L3: T List
11.
f: {T=}
12.
f TT
13.
x,y:T. f(x,y) x = y
14.
z: T
15.
z(f) L1
(z:T. z(f) nil z(eq) L3) z(eq) nil z(eq) L3
By:
Rewrite (HigherC is_member_unrollC THENC HigherC assert_evalC) 0
Generated subgoals:
None
About:
