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

At: list-dec wf 1
1. L: List
2. i: ||L||
3. 0 < L[i]
4. j: ||L||
5. j = i
0L[j]-1
By: HypSubst' -1 0
Generated subgoals:

None

About:
listintnatural_numbersubtractless_thanequal

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