Nuprl - Proof: list append ind 1 2

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

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. z : T
7. zs : T List
8. Q(zs)

Q(z.zs)

By:	RWH cons_to_appendC 0 THEN HypBackchain

Generated subgoals:

None

About:

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