1. A : Type
2. eq : EqDecider(A)
3. B : AType
4. f : a:A fp-> B(a)
5. g : a:A fp-> B(a)
6. h : a:A fp-> B(a)
7. x:A. x  dom(h) & x  dom(f)  h(x) = f(x)
8. x:A. x  dom(h) & x  dom(g)  h(x) = g(x)
9. x : A
10. x  dom(h)
11. x  dom(f  g)
12. x  dom(f)
  x  dom(g)

By:	(RWO (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) (-2) THEN (Analyze -2)

None

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