(7steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
int
upper
ind
1
1.
i:
2.
E:
{i...}
Prop
3.
E(i)
4.
k:{i+1...}. E(k-1)
E(k)
k:{i...}. E(k)
By:
BackThruLemmaWithUnfolds
Thm*
n:
. WellFnd{i}({n...};x,y.x < y) [`wellfounded`]
Generated subgoal:
1
j:{i...}. (
k:{i...}. k < j
E(k))
E(j)
About:
(7steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
j:{i...}. (k:{i...}. k < j 
E(k)) E(j)
Propk:{i+1...}. E(k-1) E(k) k:{i...}. E(k)n:. WellFnd{i}({n...};x,y.x < y)
[`wellfounded`] j:{i...}. (k:{i...}. k < j E(k)) E(j)
