Nuprl - Proof: length append 1

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

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

||as @ bs|| = ||as||+||bs||

By:	ListInd 2 THEN AbReduce 0

Generated subgoals:

None

About:

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