2. as: T*
3. i: {0...||as||}
4. j: {i...||as||}
5. k: {j...||as||}
((as[i..j
]) @ (as[j..k])) = (as[i..k]) 
T:Type, as:T*, i:{0...||as||}, j:{i...||as||}, k:{j...||as||}.
((as[i..j]) @ (as[j..k])) = (as[i..k])| 1 | 1. T: Type 2. as: T* 3. i: {0...||as||} 4. j: {i...||as||} 5. k: {j...||as||} ((as[i..j]) @ (as[j..k])) = (as[i..k]) |
About:
 |  |  |  |  |