(10steps total) PrintForm Definitions array 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: array shift wf 1
1. T : Type
2. i : 
3. j : {i...}
4. a : [T]Array{i..j}
5. m : 
  a[++m]  [T]Array{i+m..j+m}
By: Analyze 4 THEN AbSetMemEqTypeCD

Generated subgoals:

1 4. a : [T]Array 
5. a.l = i & a.u = j
6. m : 
  a[++m]  [T]Array 
6 steps
2 4. a : [T]Array 
5. a.l = i & a.u = j
6. m : 
  a[++m].l = i+m & a[++m].u = j+m
2 steps

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

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