(7steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
int
upper
ind
1
1
1
1
1.
i:
2.
E:
{i...}
Prop
3.
E(i)
4.
k:{i+1...}. E(k-1)
E(k)
5.
j:
{i...}
6.
k:{i...}. k < j
E(k)
7.
j = i
E(j)
By:
Assert (j = i)
Generated subgoal:
1
8.
j = i
{i...}
E(j)
About:
(7steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
{i...}
E(j)
Prop
k:{i+1...}. E(k-1) 
E(k)k:{i...}. k < j E(k) E(j) {i...} E(j)
