(6steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
int
lower
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:
(6steps)
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)
