At:
sublist iff assert sublist 2 x1211
1.
T: Type
2.
L: T List
3.
M: T List
4.
eq: {T=}
5.
eq TT
6.
x,y:T. eq(x,y) x = y
7.
u: T
8.
v: T List
9.
(u(eq) Mxv.x(eq) M) u(eq) M & xv.x(eq) M
10.
u(eq) M & v(eq)M
u(eq) Mxv.x(eq) M
By:
HypBackchain
Generated subgoal:
x
v.x(
T
x = y
eq)M
