(10steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: maximal-in-list
  A:Type, f:(A), L:A List. 0<||L||  (aL.(xL.f(x)f(a)))
By: InductionOnList THEN Reduce 0

Generated subgoal:

1 1. A : Type
2. f : A
3. A List
4. u : A
5. v : A List
6. 0<||v||  (av.(xv.f(x)f(a)))
7. 0<||v||+1
  (a[u / v].(x[u / v].f(x)f(a)))
9 steps

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

(10steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc