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
  x  dom(h) & x  dom(f  g)  h(x) = f  g(x)  B(x)

By:	Auto THEN RWO Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A. Thm* x  dom(f  g)  f  g(x) = if x  dom(f) f(x) else g(x) fi  B(x) 0 THEN SplitOnConclITE THEN BackThruSomeHyp

1

10. x  dom(h) 11. x  dom(f  g) 12. x  dom(f)   x  dom(g)

1 step

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