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

At: arrows wf
r:, k:, L: List. r- > L^k Prop
By: Unfold `arrows` 0
Generated subgoal:

11. r:
2. k:
3. L: List
4. n:
5. rn
6. G: {s:(n List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }||L||
7. c: ||L||
8. f: L[c]n
9. increasing(f;L[c])
10. s: L[c] List
11. ||s|| = k
12. x,y:||s||. x < y s[x] < s[y]
map(f;s) {s:(n List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }		2 steps

About:
listintnatural_numberless_thanset
equalmemberpropimpliesandall

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