Nuprl - Proof: append assoc 1

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

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

((as @ bs) @ cs) = (as @ bs @ cs)

By:	ListInd 2 THEN AbReduce 0

Generated subgoals:

1 (bs @ cs) = (bs @ cs)
Auto

2 5. u : T
6. v : T List
7. ((v @ bs) @ cs) = (v @ bs @ cs)
u.((v @ bs) @ cs) = u.(v @ bs @ cs)
1 step

About:

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

1	(bs @ cs) = (bs @ cs)	Auto
2	5. u : T 6. v : T List 7. ((v @ bs) @ cs) = (v @ bs @ cs) u.((v @ bs) @ cs) = u.(v @ bs @ cs)	1 step