m:
, n:(m+1). upto(m) ~ (upto(n) @ map(
x.x+n;upto(m-n)))l:T List. (l @ nil) ~ las,bs,cs:Top List. ((as @ bs) @ cs) ~ (as @ bs @ cs)f,as':Top, A:Type, as:A List. map(f;as @ as') ~ (map(f;as) @ map(f;as'))| Theorem | Name |
| m:, n:(m+1). upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n))) | [upto_decomp] |
| cites the following: | |
| l:T List. (l @ nil) ~ l | [append_nil_sq] |
| as,bs,cs:Top List. ((as @ bs) @ cs) ~ (as @ bs @ cs) | [append_assoc_sq] |
| f,as':Top, A:Type, as:A List. map(f;as @ as') ~ (map(f;as) @ map(f;as')) | [map_append_sq] |