(15steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
append
functionality
wrt
sublist
1
1
1
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.
L3(
eq)L4
nil(
eq)L2
(nil @ L3)(
eq)(L2 @ L4)
By:
Reduce 0
Generated subgoal:
1
True
L3(
eq)(L2 @ L4)
About:
(15steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
True 
L3(
eq)(L2 @ L4)
}
T
T
x:T. eq(x,x)
x,y:T. eq(x,y) 
eq(y,x)
x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
eq)L4
nil(eq)L2 (nil @ L3)(eq)(L2 @ L4)
True L3(eq)(L2 @ L4)
