(7steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc

At: upto wf 2 2
1. d,i,j:. j-i = d upto(i;j) {i..j} List
2. i:
3. j:
4. i < j
upto(i;j) {i..j} List
By:
RecUnfold `upto` 0
THEN
SplitOnConclITE
Generated subgoals:

None

About:
listintsubtractless_thanequalmemberimpliesall

(7steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc