Nuprl - Proof: append wf 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: append wf 1

1. T : Type
2. as : T List
3. bs : T List

(as @ bs)

T List

By:

ListInd 2

Generated subgoals:

1   (nil @ bs)  T List
1 step

2 4. u : T
5. v : T List
6. (v @ bs)  T List
  ((u.v) @ bs)  T List
2 steps

About:

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

1	(nil @ bs) T List	1 step
2	4. u : T 5. v : T List 6. (v @ bs) T List ((u.v) @ bs) T List	2 steps