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