(13steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
sublist
iff
assert
sublist
2
1
2
1.
T:
Type
2.
Discrete{T}
3.
eq:
{T
}
4.
L:
T List
5.
u:
T
6.
v:
T List
7.
M:T List. v(
eq)M
(
eq)(v,M)
M:T List. (u.v)(
eq)M
(
eq)(u.v,M)
By:
Analyze 0
Generated subgoal:
1
8.
M:
T List
(u.v)(
eq)M
(
eq)(u.v,M)
About:
(13steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
(u.v)(
eq)M 
(
eq)(u.v,M)
}
M:T List. v(eq)M (eq)(v,M)
M:T List. (u.v)(eq)M (eq)(u.v,M)
(u.v)(eq)M (eq)(u.v,M)
