(4steps total) PrintForm Definitions mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: cons one one
  T:Type, a,a':T, b,b':T List. [a / b] = [a' / b']  a = a' & b = b'
By: Unfold `guard` 0

Generated subgoals:

1 1. T : Type
2. a : T
3. a' : T
4. b : T List
5. b' : T List
6. [a / b] = [a' / b']
  a = a'
1 step
2 1. T : Type
2. a : T
3. a' : T
4. b : T List
5. b' : T List
6. [a / b] = [a' / b']
  b = b'
1 step
3 1. T : Type
2. a : T
3. a' : T
4. b : T List
5. b' : T List
6. a = a'
7. b = b'
  [a / b] = [a' / b']
1 step

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

(4steps total) PrintForm Definitions mb list 1 Sections MarkB generic Doc