Nuprl - Proof: array append wf 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
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

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html