is mentioned by

Thm* i,j:. no_repeats(;upto(i;j))	[no_repeats_upto]
Thm* n:, f,x:Top. primrec(n;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n))	[primrec_list_accum]
Thm* i,j,k:. ij jk (upto(i;k) ~ (upto(i;j) @ upto(j;k)))	[append_upto]
Thm* i,j:, k:(j-i). upto(i;j)[k] = i+k	[select_upto]
Thm* j:, i:j. ||upto(i;j)|| = j-i	[length_upto]
Thm* i,j,k:. (k upto(i;j)) ik & k < j	[member_upto]
Thm* i,j:. upto(i;j) List	[upto_int_wf]

Try larger context: Graphs