At:
sublist iff assert sublist 2
1
2
1
1
1
2
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.
L: T List
9.
u: T
10.
v: T List
11.
M: T List
12.
u(eq) M
13.
v(
eq)M
14.
v(eq)M (eq)(v,M)
xv.x(eq) M
By:
Unfold `sublist_2` -1
THEN
Reduce -1
THEN
HypBackchain
Generated subgoals:
None
About:
