(9steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
append
commutes
under
sublist
1
1
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.
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)
By:
Using [`eq',EQ] (BackThru
Thm*
eq:{T=
}, P:(T
Prop), L:T List.
x
L.P(x)
(
z:T. z(
eq) L
P(z)))
Generated subgoal:
1
z:T. z(
EQ) (L @ M)
z(
eq) (M @ L)
About:
(9steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc