Nuprl - Proof: firstn append 1

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

1. Top List

L2:Top List, n:

(Case of L2

(Canil

nil

(Caa.as'

if 0<

[a / firstn(n-1;as')] else nil fi) ~ nil

By:	Auto THEN Analyze -2 THEN Reduce 0 THEN Try Trivial THEN SplitOnConclITE

Generated subgoals:

None

About:

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