Nuprl - Proof: list append ind 1

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

1. T : Type
2. Q : (T List)

Prop
3. Q(nil)
4.

x:T. Q([x])
5.

ys,ys':T List. Q(ys)

Q(ys')

Q(ys @ ys')
6. zs : T List

Q(zs)

By:	OnVar `zs' ListIndA

Generated subgoals:

1 Q(nil)
Trivial

2 6. z : T
7. zs : T List
8. Q(zs)
Q(z.zs)
1 step

About:

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

1	Q(nil)	Trivial
2	6. z : T 7. zs : T List 8. Q(zs) Q(z.zs)	1 step