Nuprl - Proof: cons iseg 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: cons iseg 2

1. T : Type
2. a : T
3. b : T
4. l1 : T List
5. l2 : T List
6. l : T List
7. [b / l2] = ([a / l1] @ l)

l:T List. l2 = (l1 @ l)

By:	Assert ([b / l2] = ([a / l1] @ l))

Generated subgoals:

1   [b / l2] = ([a / l1] @ l)  T List
1 step

2 8. [b / l2] = ([a / l1] @ l)  T List
  l:T List. l2 = (l1 @ l)
2 steps

About:

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

1	[b / l2] = ([a / l1] @ l) T List	1 step
2	8. [b / l2] = ([a / l1] @ l) T List l:T List. l2 = (l1 @ l)	2 steps