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')

By:	RWO Thm* x,y:T. x before y  nil  False 0 THEN ExRepD

None

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