(6steps total) PrintForm Definitions array 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: array seg wf 1

1. T : Type
2. i : 
3. j : {i...}
4. a : [T]Array{i..j}
5. m : {i..j}
6. n : {m..j}
  a[m..n [T]Array{m..n}


By: Analyze 4 THEN AbSetMemEqTypeCD


Generated subgoals:

1 4. a : [T]Array 
5. a.l = i & a.u = j
6. m : {i..j}
7. n : {m..j}
  a[m..n [T]Array 

3 steps
2 4. a : [T]Array 
5. a.l = i & a.u = j
6. m : {i..j}
7. n : {m..j}
  a[m..n].l = m & a[m..n].u = n

1 step

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

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