'c,'b,'a:S, f:('a'c), g:('b'c).
  (h:(('a+'b)'c). 
  (h o (x:'a. inl(x)) = f  'a'c & h o (x:'b. inr(x)) = g  'b'c)
  & (h,y:(('a+'b)'c).
  & (h o (x:'a. inl(x)) = f  'a'c & h o (x:'b. inr(x)) = g  'b'c
  & (& y o (x:'a. inl(x)) = f  'a'c
  & (& y o (x:'b. inr(x)) = g  'b'c
  & (
  & (h = y)

None

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