(3steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: l all reduce
  T:Type, L:T List, P:(T). (xL.P(x))  reduce(x,y. P(x)y;true;L)
By: RepeatFor 2 (Analyze 0) THEN ListInd -1 THEN Reduce 0

Generated subgoals:

1 1. T : Type
2. T List
  P:(T). (xnil.P(x))  True
1 step
2 1. T : Type
2. T List
3. u : T
4. v : T List
5. P:(T). (xv.P(x))  reduce(x,y. P(x)y;true;v)
  P:(T). (x[u / v].P(x))  (P(u)reduce(x,y. P(x)y;true;v))
1 step

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

(3steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc