(9steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
append
commutes
under
sublist
1
1
1.
T:
Type
2.
Discrete{T}
3.
eq:
{T
}
4.
L:
T List
5.
M:
T List
x
(L @ M).x(
eq) (M @ L)
By:
FwdThru
Thm*
Discrete{T}
(
f:{T=
}. True) [2]
THEN
Analyze -1
THEN
Thin -1
THEN
RenameVar `EQ' -1
THEN
DiscreteEq -1
THEN
Equivalence 3
Generated subgoal:
1
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.
M:
T List
10.
EQ:
{T=
}
11.
EQ
T
T
12.
x,y:T. EQ(x,y)
x = y
x
(L @ M).x(
eq) (M @ L)
About:
(9steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc