(44steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
discrete
list
1
1
2
2
2
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.
Dec(v = v1)
u.v = u1.v1
u.v = u1.v1
By:
Analyze 10
Generated subgoals:
1
10.
v = v1
u.v = u1.v1
u.v = u1.v1
2
10.
v = v1
u.v = u1.v1
u.v = u1.v1
About:
(44steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
u.v = u1.v1 
u.v = u1.v1v = v1 u.v = u1.v1 u.v = u1.v1u.v = v1
u.v = u1.v1 u.v = u1.v1
u.v = u1.v1 u.v = u1.v1v = v1 u.v = u1.v1 u.v = u1.v1
