Nuprl - Proof: array append wf 1 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: array append wf 1 1 2

1. T : Type
2. i :

3. j : {i...}
4. k : {j...}
5. a : [T]Array
6. a.l = i
7. a.u = j
8. b : [T]Array
9. b.l = j
10. b.u = k

a @ b.l = i & a @ b.u = k

By:	OnHyps [8;9;5;6] Analyze THEN Unfold `array_append` 0 THEN OnAllClauses AbReduce

Generated subgoal:

1 5. n1 :
6. m1 : {n1...}
7. {n1..m1}T
8. n1 = i
9. m1 = j
10. n :
11. m : {n...}
12. {n..m}T
13. n = j
14. m = k
n1 = i & m = k
Auto

About:

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