At: array append wf 1 1 1 1
1. T: Type
2. i: 
3. j: {i...}
4. k: {j...}
5. n1:
6. m1: {n1...}
7. a2: {n1..m1
}
T
8. n1 = i
9. m1 = j
10. n:
11. m: {n...}
12. b2: {n..m}T
13. n = j
14. m = k
< n1,m,(
i.if i < m1
a2(i) ; b2(i) fi) > 
[T]Array
By: Unfold `array` 0
Generated subgoals:None