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

None

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