(13steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
sublist
iff
assert
sublist
2
1
2
1
1
2
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.
u:
T
10.
v:
T List
11.
M:T List. v(
eq)M
(
eq)(v,M)
12.
M:
T List
13.
u(
eq) M
x
v.x(
eq) M
u(
eq) M
By:
RWH (LemmaC
Thm*
p,q:
. (p
q)
p & q) -1
Generated subgoals:
None
About:
(13steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
}
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)
M:T List. v(
eq)M (eq)(v,M)
eq) M
xv.x(eq) M
u(eq) M
p,q:. (pq) p & q)
-1