(13steps 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: before-map
  T,T':Type, f:(TT'), L:T List, x',y':T'.
  x' before y'  map(f;L)  (x,y:T. x before y  L & f(x) = x' & f(y) = y')
By: InductionOnList THEN Reduce 0

Generated subgoals:

1 1. T : Type
2. T' : Type
3. f : TT'
4. T List
  x',y':T'.
  x' before y'  nil  (x,y:T. x before y  nil & f(x) = x' & f(y) = y')
1 step
2 1. T : Type
2. T' : Type
3. f : TT'
4. T List
5. u : T
6. v : T List
7. x',y':T'.
7. x' before y'  map(f;v)  (x,y:T. x before y  v & f(x) = x' & f(y) = y')
  x',y':T'.
  x' before y'  [(f(u)) / map(f;v)]
  
  (x,y:T. x before y  [u / v] & f(x) = x' & f(y) = y')
11 steps

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

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