A:Type, eq:EqDecider(A), f,g:a:A fp-> Top, x:A.
  x  dom(f  g)  x  dom(f)  x  dom(g)

By:	UnivCD THEN Inst Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A. Thm* x  dom(f  g)  x  dom(f)  x  dom(g) [A;a. Top;eq;f;g;x] THEN Try Trivial

None

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