(6steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
int
lower
ind
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)
E(j)
By:
Decide (j = i)
Generated subgoals:
1
7.
j = i
E(j)
2
7.
j = i
E(j)
About:
(6steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
E(j)
j = i E(j)
Prop
k:{...i-1}. E(k+1) 
E(k)k:{...i}. k > j E(k) E(j) E(j)j = i E(j)
