A,A':Type.
  strong-subtype(A;A')
  
  (B:(AType), C:(A'Type), eq:EqDecider(A), eq':EqDecider(A'),
  (f,g:a:A fp-> B(a). (a:A. B(a) r C(a))  f  g  f  g)

None

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html