(7steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
int
upper
ind
i:
, E:({i...}
Prop). E(i)
(
k:{i+1...}. E(k-1)
E(k))
(
k:{i...}. E(k))
By:
UnivCD
Generated subgoal:
1
1.
i:
2.
E:
{i...}
Prop
3.
E(i)
4.
k:{i+1...}. E(k-1)
E(k)
k:{i...}. E(k)
About:
(7steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
Prop
k:{i+1...}. E(k-1) 
E(k)
k:{i...}. E(k) i:, E:({i...}Prop). E(i) (k:{i+1...}. E(k-1) E(k)) (k:{i...}. E(k))Propk:{i+1...}. E(k-1) E(k) k:{i...}. E(k)
