(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 2 1
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')
8. x' : T'
9. y' : T'
10. x' = f(u) & (y'  map(f;v))  x' before y'  map(f;v)
  x,y:T. x = u & (y  v)  x before y  v & f(x) = x' & f(y) = y'
By: SplitOrHyps THEN ExRepD

Generated subgoals:

1 10. x' = f(u)
11. (y'  map(f;v))
  x,y:T. x = u & (y  v)  x before y  v & f(x) = x' & f(y) = y'
2 steps
2 10. x' before y'  map(f;v)
  x,y:T. x = u & (y  v)  x before y  v & f(x) = x' & f(y) = y'
2 steps

About:
listapplyfunctionuniverseequalandorallexists
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