(44steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
discrete
list
1
1
2
2
2
1
1
1
1.
T:
Type
2.
Discrete{T}
3.
x:
T List
4.
u:
T
5.
v:
T List
6.
y:
T List
7.
u1:
T
8.
v1:
T List
9.
u.v = v1
10.
v = v1
u.v = u1.v1
u.v = u1.v1
By:
FwdThru
Thm*
Discrete{T}
(
f:(T
T
).
x,y:T. f(x,y)
x = y) [2]
THEN
Analyze -1
Generated subgoal:
1
11.
f:
T
T
12.
x,y:T. f(x,y)
x = y
T
u.v = u1.v1
u.v = u1.v1
About:
(44steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
T
x,y:T. f(x,y) 
x = y 
T
u.v = u1.v1 
u.v = u1.v1u.v = v1
u.v = u1.v1 u.v = u1.v1
(
f:(TT). x,y:T. f(x,y) x = y)
[2]
Tx,y:T. f(x,y) x = y T u.v = u1.v1 u.v = u1.v1
