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