Nuprl - Proof: append firstn lastn

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: append firstn lastn

T:Type, L:T List, n:{0...||L||}. (firstn(n;L) @ nth_tl(n;L)) = L

By:	RepeatFor 2 (Analyze 0) THEN ListInd -1 THEN RecUnfold `firstn` 0 THEN RecUnfold `nth_tl` 0 THEN Reduce 0 THEN SplitOnConclITE THEN SplitOnConclITE THEN Reduce 0 THEN Analyze THEN EasyHyp

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html