At:
append functionality wrt sublist
1
1
1
1
1
2
2
1.
T: Type
2.
L1: T List
3.
L2: T List
4.
eq: {T
}
5.
eq 
T
T
6.
x:T. eq(x,x)
7.
x,y:T. eq(x,y) 
eq(y,x)
8.
x,y,z:T. eq(x,y) 
eq(y,z) eq(x,z)
9.
L3: T List
10.
L4: T List
11.
Discrete{T}
12.
u: T
13.
v: T List
14.
v(
eq)L4 v(eq)(L2 @ L4)
15.
u(eq) L4
16.
v(eq)L4
v(eq)(L2 @ L4)
By:
HypBackchain
Generated subgoals:
None
About:
