(7steps total) PrintForm Definitions array 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: array append wf 1 1 1
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  [T]Array 
By: OnHyps [8;9;5;6] Analyze THEN Unfold `array_append` 0 THEN OnAllClauses AbReduce

Generated subgoal:

1 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 
1 step

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

(7steps total) PrintForm Definitions array 1 Sections StandardLIB Doc